Expressiveness of propositional projection temporal logic with star

DOI10.1016/j.tcs.2010.12.047zbMath1221.03018OpenAlexW2037296871MaRDI QIDQ2430015

Zhenhua Duan, Cong Tian

Publication date: 5 April 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.047

zbMATH Keywords

verificationautomata theoryregular expressionsregular languagetemporal logicexpressivenessBüchi automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Equational classes, universal algebra in model theory (03C05)

Related Items (13)

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 of pushdown systems for projection temporal logic ⋮ Efficient decision procedure for propositional projection temporal logic ⋮ A sound and complete proof system for a unified temporal logic ⋮ Verification of distributed systems with the axiomatic system of MSVL ⋮ Temporal logic specification mining of programs ⋮ A decision procedure and complete axiomatization for projection temporal logic ⋮ Model checking Petri nets with MSVL ⋮ A formal proof of the deadline driven scheduler in PPTL axiomatic system ⋮ Extending MSVL with Semaphore ⋮ Index set expressions can represent temporal logic formulas ⋮ PPTL specification mining based on LNFG

Uses Software

• SPIN

Cites Work

• Framed temporal logic programming
• A decision procedure for propositional projection temporal logic with infinite models
• Temporal logic can be more expressive
• Complexity of propositional projection temporal logic with star
• 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

This page was built for publication: Expressiveness of propositional projection temporal logic with star