Checking Temporal Properties of Discrete, Timed and Continuous Behaviors

DOI10.1007/978-3-540-78127-1_26zbMath1133.68378OpenAlexW1494737186MaRDI QIDQ5452193

Amir Pnueli, Dejan Ničković, Oded Maler

Publication date: 25 March 2008

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

Full work available at URL: https://doi.org/10.1007/978-3-540-78127-1_26

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Combining refinement and signal-temporal logic for biological systems ⋮ Model Checking of Biological Systems ⋮ Bounded variability of metric temporal logic ⋮ Extracting counterexamples induced by safety violation in linear hybrid systems ⋮ From LTL to rLTL monitoring: improved monitorability through robust semantics ⋮ HRELTL: a temporal logic for hybrid systems ⋮ A program logic to verify signal temporal logic specifications of hybrid systems ⋮ Unnamed Item ⋮ STL*: extending signal temporal logic with signal-value freezing operator ⋮ TeLEx: learning signal temporal logic from positive examples using tightness metric ⋮ On simulation-based probabilistic model checking of mixed-analog circuits ⋮ Analog property checkers: a DDR2 case study ⋮ Parameter Synthesis Through Temporal Logic Specifications ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Parameter synthesis of polynomial dynamical systems

Uses Software

• FoCs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of timed automata
• A compositional approach to CTL\(^*\) verification
• On Bounded Specifications
• Timed regular expressions
• From MITL to Timed Automata
• The benefits of relaxing punctuality
• Model Checking Software
• Fault Diagnosis for Timed Automata
• On Synthesizing Controllers from Bounded-Response Properties
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal Modeling and Analysis of Timed Systems
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• Computer Aided Verification