Specification in CTL + past for verification in CTL.

DOI10.1006/inco.1999.2817zbMath1046.68599OpenAlexW2059221592MaRDI QIDQ1854327

Yanyan Li

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1999.2817

zbMATH Keywords

temporal logicPCTLmodel-checking specificationsNCTL

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (15)

Model-checking CTL* over flat Presburger counter systems ⋮ Temporal Logic and Fair Discrete Systems ⋮ On the Hybrid Extension of CTL and CTL + ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ \textit{Once} and \textit{for all} ⋮ Alternating-time temporal logics with linear past ⋮ Unnamed Item ⋮ Quantification over sets of possible worlds in branching-time semantics ⋮ Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions ⋮ The Complexity of CTL* + Linear Past ⋮ On the Complexity of Branching-Time Logics ⋮ An axiomatization of PCTL* ⋮ Branching-time logics repeatedly referring to states ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Taming past LTL and flat counter systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A hierarchy of temporal logics with past
• Symbolic model checking: \(10^{20}\) states and beyond
• Up and Down The Temporal Way
• Buy one, get one free!!!
• Interpolants and Symbolic Model Checking

This page was built for publication: Specification in CTL + past for verification in CTL.