A temporal logic for micro- and macro-step-based real-time systems: foundations and applications

DOI10.1016/j.tcs.2016.06.042zbMath1348.68149OpenAlexW2462399399MaRDI QIDQ530560

Dino Mandrioli, Luca Ferrucci, Angelo Morzenti, Matteo Rossi

Publication date: 1 August 2016

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2016.06.042

zbMATH Keywords

Petri netsformal verificationnonstandard analysisautomatic verificationmetric temporal logicmicro- and macro-stepsStateflow/Simulink

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) Other applications of nonstandard models (economics, physics, etc.) (03H10)

Uses Software

• PVS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Non-standard semantics of hybrid systems modelers
• Constraint LTL satisfiability checking without automata
• Real-time logics: Complexity and expressiveness
• Modeling time in computing.
• A timeband framework for modelling real-time systems
• Statecharts: a visual formalism for complex systems
• Dealing with zero-time transitions in axiom systems.
• A propositional linear time logic with time flow isomorphic to \(\omega^2\)
• Prefix and Projection onto State in Duration Calculus
• A theory of sampling for continuous-time metric temporal logic
• Some Recent Results in Metric Temporal Logic
• Modelling of Complex Systems: Systems as Dataflow Machines
• Constraint logic programming for reasoning about discrete event processes
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• A really temporal logic
• The benefits of relaxing punctuality
• Compositional Verification of Quantitative Properties of Statecharts
• Robustness of Time Petri Nets under Guard Enlargement
• Robustness in Timed Automata
• What good are digital clocks?
• Lectures on Concurrency and Petri Nets
• Modeling Timed Concurrent Systems
• Foundations of Software Science and Computation Structures

This page was built for publication: A temporal logic for micro- and macro-step-based real-time systems: foundations and applications