Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems

DOI10.1007/978-3-642-04420-5_11zbMath1260.68229OpenAlexW2102281969MaRDI QIDQ3646256

Ivan S. Zapreev, Peter J. Collins

Publication date: 19 November 2009

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

Full work available at URL: https://ir.cwi.nl/pub/13946

zbMATH Keywords

model checkingcomputabilitydynamic systemsCTL\( ^{*}\)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Abstract and axiomatic computability and recursion theory (03D75)

Related Items (1)

Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems

Uses Software

• Ariadne

Cites Work

• Dynamic topological logic
• Results on the propositional \(\mu\)-calculus
• Verification of reactive systems. Formal methods and algorithms.
• Computability on subsets of metric spaces.
• Continuity and computability of reachable sets
• Optimal semicomputable approximations to reachable and invariant sets
• COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS
• Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• On the Continuity of Effective Multifunctions
• From linear time to branching time
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Computable CTL * for Discrete-Time and Continuous-Space Dynamic Systems