Characterization of temporal property classes

DOI10.1007/3-540-55719-9_97MaRDI QIDQ5204340zbMATH OpenOpenAlexFDO

Authors

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_97

zbMATH Keywords

temporal logicproof ruletemporal formulaliveness propertyseparate property

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Recognizing safety and liveness
• Safety, liveness and fairness in temporal logic
• A lattice-theoretic characterization of safety and liveness
• scientific article; zbMATH DE number 139631
• scientific article; zbMATH DE number 1059326

Cites work

• scientific article; zbMATH DE number 4153903 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• Defining liveness
• Is the Interesting Part of Process Logic uninteresting?: A Translation from PL to PDL
• Proving the Correctness of Multiprocess Programs
• Recognizing safety and liveness

Cited in

(26)

• An Operational Guide to Monitorability
• A first-order logic characterization of safety and co-safety languages
• A topological characterization of weakness
• scientific article; zbMATH DE number 1536568 (Why is no real title available?)
• Reactive safety
• A simple rewrite system for the normalization of linear temporal logic
• Monitorability for the Hennessy-Milner logic with recursion
• Back to the future: a fresh look at linear temporal logic
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Semantics of temporal classes
• A hierarchy of temporal logics with past
• Efficient reactive synthesis using mode decomposition
• Mathematical Foundations of Computer Science 2003
• A first-order logic characterisation of safety and co-safety languages
• Synthesising correct concurrent runtime monitors
• Towards the exact complexity of realizability for safety LTL
• Succinctness of cosafety fragments of LTL via combinatorial proof systems
• Towards an efficient implementation of a tableau method for reactive safety specifications
• Expressiveness of extended bounded response \textsf{LTL}
• scientific article; zbMATH DE number 139631 (Why is no real title available?)
• Time-triggered runtime verification
• Safety, liveness and fairness in temporal logic
• Runtime enforcement of timed properties using games
• On the translation of automata to linear temporal logic
• Sooner is safer than later
• Aspect Categories and Classes of Temporal Properties

This page was built for publication: Characterization of temporal property classes

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