An Automata-based Approach for CTL⋆ With Constraints

DOI10.1016/j.entcs.2009.05.040zbMath1347.68224OpenAlexW1974406548MaRDI 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 checkingtemporal logicautomata approach

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (4)

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

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

This page was built for publication: An Automata-based Approach for CTL⋆ With Constraints