COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS

DOI10.1142/S012905411100843XzbMath1238.68084OpenAlexW1981881367MaRDI QIDQ3016218

Ivan S. Zapreev, Peter J. Collins

Publication date: 14 July 2011

Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1142/s012905411100843x

zbMATH Keywords

model checkingtemporal logiccomputabilitydynamic systemscontinuous state spaceLTLCTL\(\text{CTL}^*\)

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (1)

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

Cites Work

• Dynamic topological logic
• Computability on subsets of metric spaces.
• Continuity and computability of reachable sets
• Optimal semicomputable approximations to reachable and invariant sets
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• On the Continuity of Effective Multifunctions

This page was built for publication: COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS