On the expressivity and complexity of quantitative branching-time temporal logics

DOI10.1016/S0304-3975(02)00644-8zbMath1019.03012MaRDI QIDQ1401306

D. Massart

Publication date: 17 August 2003

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

zbMATH Keywords

complexitydiscrete timemodel checkingexpressivityCTLbranching-time temporal logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (6)

Efficient timed model checking for discrete-time systems ⋮ On the complexity of verification of time-sensitive distributed systems ⋮ A new model for model checking: cycle-weighted Kripke structure ⋮ Model checking and synthesis for branching multi-weighted logics ⋮ Logical formalism for specification of real-time multiagent systems ⋮ Model checking MASL specification of distributed real-time systems

Uses Software

• NuSMV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• Characterizing finite Kripke structures in propositional temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• The complexity of propositional linear temporal logics in simple cases
• NuSMV: A new symbolic model checker
• Is your model checker on time? On the complexity of model checking for timed modal logics
• On programming of arithmetic operations
• A really temporal logic
• An automata-theoretic approach to branching-time model checking

This page was built for publication: On the expressivity and complexity of quantitative branching-time temporal logics