Checking Temporal Properties of Discrete, Timed and Continuous Behaviors

DOI10.1007/978-3-540-78127-1_26MaRDI QIDQ5452193zbMATH OpenOpenAlexFDO

Authors Oded Maler, Dejan Ničković, Amir Pnueli

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

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

Recommendations

• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Algorithms for monitoring real-time properties
• Model-checking timed temporal logics
• Some Recent Results in Metric Temporal Logic
• Monitoring temporal logic with clock variables

Cites work

• A compositional approach to CTL^* verification
• A theory of timed automata
• An improved on-the-fly tableau construction for a real-time temporal logic.
• Fault diagnosis for timed automata
• Formal Modeling and Analysis of Timed Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• From MITL to Timed Automata
• scientific article; zbMATH DE number 1670800 (Why is no real title available?)
• scientific article; zbMATH DE number 1696514 (Why is no real title available?)
• scientific article; zbMATH DE number 5604117 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 1303069 (Why is no real title available?)
• scientific article; zbMATH DE number 1304997 (Why is no real title available?)
• scientific article; zbMATH DE number 2080059 (Why is no real title available?)
• scientific article; zbMATH DE number 2112984 (Why is no real title available?)
• scientific article; zbMATH DE number 3186872 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Model Checking Software
• On bounded specifications
• On Synthesizing Controllers from Bounded-Response Properties
• Reasoning with temporal logic on truncated paths.
• The benefits of relaxing punctuality
• Timed regular expressions

Cited in

(30)

• Monitoring temporal logic with clock variables
• Algorithms for monitoring real-time properties
• Combining the temporal and epistemic dimensions for MTL monitoring
• TeLEx: learning signal temporal logic from positive examples using tightness metric
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Parameter synthesis of polynomial dynamical systems
• Extracting counterexamples induced by safety violation in linear hybrid systems
• Combining refinement and signal-temporal logic for biological systems
• Bounded variability of metric temporal logic
• STL*: extending signal temporal logic with signal-value freezing operator
• A Domain View of Timed Behaviors
• Trace diagnostics using temporal implicants
• Robust Sampling for MITL Specifications
• scientific article; zbMATH DE number 67858 (Why is no real title available?)
• scientific article; zbMATH DE number 1304310 (Why is no real title available?)
• Specifying timed patterns using temporal logic
• Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract)
• Parameter synthesis through temporal logic specifications
• Model checking of biological systems
• Monitoring Temporal Properties of Stochastic Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Verification, Model Checking, and Abstract Interpretation
• On simulation-based probabilistic model checking of mixed-analog circuits
• Analog property checkers: a DDR2 case study
• From LTL to rLTL monitoring: improved monitorability through robust semantics
• A program logic to verify signal temporal logic specifications of hybrid systems
• A bounded model checking technique for discrete-time nonlinear systems
• Verifying linear temporal properties on polyhedral systems: decidability and symbolic algorithms
• It's about time: temporal references in emergent communication
• HRELTL: a temporal logic for hybrid systems

Describes a project that uses

Uses Software

• FoCs

This page was built for publication: Checking Temporal Properties of Discrete, Timed and Continuous Behaviors

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