Proving properties of continuous systems: Qualitative simulation and temporal logic

DOI10.1016/S0004-3702(96)00050-1MaRDI QIDQ1402734zbMATH OpenOpenAlexFDO

Authors Benjamin Shults, Benjamin J. Kuipers

Publication date 28 August 2003

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0004-3702(96)00050-1

zbMATH Keywords

Differential equationsModel checkingQualitative simulationTemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Error bounds for numerical methods for ordinary differential equations (65L70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Focusing qualitative simulation using temporal logic: Theoretical foundations
• scientific article; zbMATH DE number 1759607
• A proof-based method for modelling timed systems
• Temporal proof methodologies for timed transition systems
• scientific article; zbMATH DE number 15894
• The intuitionistic temporal logic of dynamical systems
• On the decidability of continuous time specification formalisms
• Verification of continuous dynamical systems by timed automata
• scientific article; zbMATH DE number 1614646
• Deductive verification of continuous dynamical systems

Cites work

• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• Qualitative simulation
• Real-time logics: Complexity and expressiveness
• The composition and validation of heterogeneous control laws

Cited in

(10)

• Focusing qualitative simulation using temporal logic: Theoretical foundations
• An axiomatic approach to existence and liveness for differential equations
• Pegasus: sound continuous invariant generation
• Deductive stability proofs for ordinary differential equations
• Abstractions for hybrid systems
• Monitoring bounded LTL properties using interval analysis
• Random generation of monotonic functions for Monte Carlo solution of qualitative differential equations
• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• Pegasus: a framework for sound continuous invariant generation
• Robustness of temporal logic specifications for continuous-time signals

This page was built for publication: Proving properties of continuous systems: Qualitative simulation and temporal logic

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