A decision procedure for propositional projection temporal logic with infinite models

DOI10.1007/s00236-007-0062-zzbMath1141.68039OpenAlexW2021917262MaRDI QIDQ2480780

Li Zhang, Cong Tian, Zhenhua Duan

Publication date: 3 April 2008

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-007-0062-z

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) Temporal logic (03B44)

Related Items

A compiler for MSVL and its applications ⋮ A temporal programming model with atomic blocks based on projection temporal logic ⋮ Operational semantics of Framed Tempura ⋮ Symbolic Model Checking for Alternating Projection Temporal Logic ⋮ A cylinder computation model for many-core parallel computing ⋮ A complete proof system for propositional projection temporal logic ⋮ A canonical form based decision procedure and model checking approach for propositional projection temporal logic ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ Model checking open systems with alternating projection temporal logic ⋮ Efficient decision procedure for propositional projection temporal logic ⋮ A sound and complete proof system for a unified temporal logic ⋮ Expressiveness of propositional projection temporal logic with star ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ Temporal logic specification mining of programs ⋮ A novel algorithm for intrusion detection based on RASL model checking ⋮ Verify heaps via unified model checking ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Verification and enforcement of access control policies ⋮ Transformation from PLTL to automata via NFGs ⋮ Unconditional secure communication: a Russian cards protocol ⋮ A note on stutter-invariant PLTL ⋮ Axiomatic semantics of projection temporal logic programs ⋮ Complexity of propositional projection temporal logic with star ⋮ Translating Xd-C programs to MSVL programs ⋮ Bounded model checking of traffic light control system ⋮ A practical decision procedure for propositional projection temporal logic with infinite models ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ Extending MSVL with Semaphore ⋮ Satisfiability of Linear Time Mu-Calculus on Finite Traces ⋮ Index set expressions can represent temporal logic formulas ⋮ Some Fixed-Point Issues in PPTL ⋮ PPTL specification mining based on LNFG ⋮ A structural transformation from p-\(\pi\) to MSVL

Uses Software

• SPIN

Cites Work

• Process logic: Expressiveness, decidability, completeness
• A calculus of durations
• Completeness of temporal logics over infinite intervals.
• Temporal logic can be more expressive
• Equations between Regular Terms and an Application to Process Logic
• A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item