An Automata-based Approach for CTL⋆ With Constraints

DOI10.1016/j.entcs.2009.05.040zbMath1347.68224MaRDI QIDQ5179062

Régis Gascon

Publication date: 19 March 2015

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.040

zbMATH Keywords

model checking; temporal logic; automata approach

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

03B44: Temporal logic

Related Items

Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints, CTL* model checking for data-aware dynamic systems with arithmetic, Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints, Satisfiability of ECTL* with Tree Constraints

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of timed automata
• Reasoning about infinite computations
• Model checking LTL with regular valuations for pushdown systems
• Towards a Model-Checker for Counter Systems
• Deciding full branching time logic
• Deciding properties of integral relational automata
• Foundations of Software Science and Computation Structures
• An automata-theoretic approach to branching-time model checking
• Automated Reasoning with Analytic Tableaux and Related Methods
• CONCUR 2005 – Concurrency Theory