Branching-time logics with path relativisation
\(\omega\)-languagesbranching-time logiccomputational complexityexpressivitymodel checkingrelativized quantifierssatisfiabilitytemporal logic
Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)
Temporal logics are a widespread tool in specification and verification of finite state systems. Branching-time logic CTL* is one of the more expressive languages used. It extends linear temporal logic, suitable to specify temporal properties along computation paths, with path quantifiers. The present paper extends CTL* by relativized quantifiers. For this, the model of finite state systems is modified by adding labels (alphabet symbols) to edges between nodes. In this way, an infinite path in the system defines an infinite word (\(\omega\)-word), its so-called \textit{trace}. The relativized path quantifiers now quantify only over such paths whose trace is an element in a fixed \(\omega\)-language.NEWLINENEWLINEDifferent classes of \(\omega\)-languages used in quantifier relativization are considered (regular, visibly pushdown, pushdown) and for each of them, expressivity, complexity of model checking, and complexity of satisfiability are studied. For example, model checking for CTL with arbitrary pushdown language remains polynomial-time decidable, model checking for CTL* relative to regular \(\omega\)-languages remains PSPACE-complete, but becomes EXPTIME-complete for more complicated path languages.
- 25 years of model checking. History, achievements, perspectives
- A CTL-based logic for program abstractions
- A decision procedure for \(\mathrm{CTL}^{*}\) based on tableaux and automata
- A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL
- Computation Tree Regular Logic for Genetic Regulatory Networks
- Counterexample-guided abstraction refinement for symbolic model checking
- Decision procedures and expressiveness in the temporal logic of branching time
- Extended computation tree logic
- Foundations of Software Science and Computation Structures
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Games for synthesis of controllers with partial observation.
- scientific article; zbMATH DE number 1705163 (Why is no real title available?)
- scientific article; zbMATH DE number 3870578 (Why is no real title available?)
- scientific article; zbMATH DE number 3983144 (Why is no real title available?)
- scientific article; zbMATH DE number 3664335 (Why is no real title available?)
- scientific article; zbMATH DE number 1048047 (Why is no real title available?)
- scientific article; zbMATH DE number 2038753 (Why is no real title available?)
- scientific article; zbMATH DE number 1500644 (Why is no real title available?)
- scientific article; zbMATH DE number 941396 (Why is no real title available?)
- scientific article; zbMATH DE number 3237829 (Why is no real title available?)
- Model checking of RegCTL
- Model Checking Software
- Model-checking in dense real-time
- Propositional dynamic logic of looping and converse is elementarily decidable
- Propositional dynamic logic of nonregular programs
- Propositional dynamic logic of regular programs
- Propositional dynamic logic with recursive programs
- Pushdown processes: Games and model-checking
- Reachability analysis of pushdown automata: Application to model-checking
- Reasoning about infinite computations
- The complexity of propositional linear temporal logics
- The Complexity of Tree Automata and Logics of Programs
- Visibly pushdown languages
- “Sometimes” and “not never” revisited
- Branching-time logics repeatedly referring to states
- R-generability, and definability in branching time logics
- A branching time logic with past operators
- Sublogics of a branching time logic of robustness
- scientific article; zbMATH DE number 4119600 (Why is no real title available?)
- Extended computation tree logic
- Finite and Circular Path Models for Branching Time Logics
- A Branching Time Variant of CaRet
- Temporal logics with language parameters
This page was built for publication: Branching-time logics with path relativisation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q386037)
