Characterization of temporal property classes

DOI10.1007/3-540-55719-9_97zbMATH Open1425.68252OpenAlexW1577761978MaRDI QIDQ5204340FDOQ5204340

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

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

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)

Cites Work

• Title not available (Why is that?)
• Defining liveness
• Proving the Correctness of Multiprocess Programs
• Recognizing safety and liveness
• Title not available (Why is that?)
• Is the Interesting Part of Process Logic uninteresting?: A Translation from PL to PDL

Cited In (26)

• A first-order logic characterization of safety and co-safety languages
• A topological characterization of weakness
• Title not available (Why is that?)
• 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
• Towards the exact complexity of realizability for safety LTL
• Synthesising correct concurrent runtime monitors
• 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}
• Title not available (Why is that?)
• 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
• An Operational Guide to Monitorability

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)