Model checking open systems with alternating projection temporal logic

DOI10.1016/j.tcs.2016.06.019zbMath1423.68293OpenAlexW2463231560MaRDI QIDQ2424878

Zhenhua Duan, Cong Tian

Publication date: 25 June 2019

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

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

zbMATH Keywords

automatamodel checkingtemporal logicopen systemsconcurrent game structures

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On equations for regular languages, finite automata, and sequential networks
• The temporal logic of branching time
• Results on the propositional \(\mu\)-calculus
• Computer science today. Recent trends and developments
• A decision procedure for propositional projection temporal logic with infinite models
• Alternating-time temporal logic
• Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
• ATL* Satisfiability Is 2EXPTIME-Complete
• Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus
• Alternation
• Verification: Theory and Practice