What good are digital clocks?

DOI10.1007/3-540-55719-9_103zbMath1425.68255OpenAlexW1572777470MaRDI QIDQ5204346

Amir Pnueli, Zohar Manna, Thomas A. Henzinger

Publication date: 4 December 2019

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-55719-9_103

zbMATH Keywords

verification methodtemporal logiclinear temporal logicatomic proposition

Mathematics Subject Classification ID

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

Related Items

Metric temporal logic revisited, Presburger liveness verification of discrete timed automata., Expected reachability-time games, Tweaking the odds in probabilistic timed automata, Model Checking Real-Time Systems, Process Algebra and Model Checking, Algorithms for monitoring real-time properties, A decidable timeout-based extension of linear temporal logic, Verification and Control of Partially Observable Probabilistic Real-Time Systems, Verification in continuous time by discrete reasoning, HRELTL: a temporal logic for hybrid systems, Cyclic-routing of unmanned aerial vehicles, Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems, Symbolic State Space of Stopwatch Petri Nets with Discrete-Time Semantics (Theory Paper), Verification and control of partially observable probabilistic systems, Some Recent Results in Metric Temporal Logic, The expressive power of clocks, On parametric timed automata and one-counter machines, Model checking for probabilistic timed automata, A temporal logic for micro- and macro-step-based real-time systems: foundations and applications, Monotonic hybrid systems, Robustness of temporal logic specifications for continuous-time signals, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, Unnamed Item, Unnamed Item, What's decidable about hybrid automata?, Timed CSP = Closed Timed Automata1, Decidable integration graphs., Entropy of regular timed languages

Uses Software

• LUSTRE
• Esterel

Cites Work

• Using mappings to prove timing properties
• Temporal proof methodologies for timed transition systems
• Formal verification of parallel programs
• A really temporal logic
• The benefits of relaxing punctuality
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item