Characterization of temporal property classes

DOI10.1007/3-540-55719-9_97zbMath1425.68252OpenAlexW1577761978MaRDI QIDQ5204340

No author found.

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) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (11)

Monitorability for the Hennessy-Milner logic with recursion ⋮ Synthesising correct concurrent runtime monitors ⋮ A simple rewrite system for the normalization of linear temporal logic ⋮ A first-order logic characterization of safety and co-safety languages ⋮ Runtime enforcement of timed properties using games ⋮ On the translation of automata to linear temporal logic ⋮ A first-order logic characterisation of safety and co-safety languages ⋮ A hierarchy of temporal logics with past ⋮ Time-triggered runtime verification ⋮ A survey of challenges for runtime verification from advanced application domains (beyond software) ⋮ Back to the future: a fresh look at linear temporal logic

Cites Work

• Defining liveness
• Recognizing safety and liveness
• Is the Interesting Part of Process Logic uninteresting?: A Translation from PL to PDL
• Proving the Correctness of Multiprocess Programs
• Unnamed Item
• Unnamed Item

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