An automata-based approach for CTL^* with constraints

DOI10.1016/J.ENTCS.2009.05.040MaRDI QIDQ5179062zbMATH OpenOpenAlexFDO

Authors 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

automata approachmodel checkingtemporal logic

Mathematics Subject Classification ID

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

Recommendations

• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• scientific article; zbMATH DE number 1954378
• Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
• An automata-theoretic approach to constraint LTL
• An automata-theoretic approach to branching-time model checking

Cites work

• A theory of timed automata
• An automata-theoretic approach to branching-time model checking
• Automated Reasoning with Analytic Tableaux and Related Methods
• CONCUR 2005 – Concurrency Theory
• Deciding full branching time logic
• Deciding properties of integral relational automata
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 1670482 (Why is no real title available?)
• scientific article; zbMATH DE number 1232241 (Why is no real title available?)
• scientific article; zbMATH DE number 1954378 (Why is no real title available?)
• scientific article; zbMATH DE number 2086598 (Why is no real title available?)
• scientific article; zbMATH DE number 2243382 (Why is no real title available?)
• Model checking LTL with regular valuations for pushdown systems
• Reasoning about infinite computations
• Towards a Model-Checker for Counter Systems

Cited in

(15)

• CTL* model checking for data-aware dynamic systems with arithmetic
• Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints
• Verification of gap-order constraint abstractions of counter systems
• Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
• Verification of gap-order constraint abstractions of counter systems
• Satisfiability of \(\mathsf {ECTL}^*\) with tree constraints
• scientific article; zbMATH DE number 1954378 (Why is no real title available?)
• Automaton-Based Criteria for Membership in CTL
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Verification, Model Checking, and Abstract Interpretation
• First steps towards taming description logics with strings
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
• Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures
• Reachability and bounded emptiness problems of constraint automata with prefix, suffix and infix
• An automata-theoretic approach to constraint LTL

This page was built for publication: An automata-based approach for \(\text{CTL}^{*}\) with constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5179062)