On relative and probabilistic finite counterability

DOI10.1007/s10703-017-0277-8zbMath1390.68433OpenAlexW2606511843MaRDI QIDQ1742987

Gal Vardi, Orna Kupferman

Publication date: 12 April 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2015/5414/

zbMATH Keywords

livenesssafetyprobabilitymodel checkingcounterexamples

Mathematics Subject Classification ID

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

Related Items (1)

On monitoring linear temporal properties

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deciding safety and liveness in TPTL
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Defining liveness
• Recognizing safety and liveness
• The temporal semantics of concurrent programs
• Sooner is safer than later
• Reasoning about infinite computations
• Safety, liveness and fairness in temporal logic
• From pre-historic to post-modern symbolic model checking
• A Note on Monitors and Büchi Automata
• Synthesis of Trigger Properties
• Spanning the Spectrum from Safety to Liveness
• On the Construction of Fine Automata for Safety Properties
• The complexity of propositional linear temporal logics
• Proving Liveness Properties of Concurrent Programs
• The complexity of probabilistic verification
• Probably safe or live
• A Framework for Ranking Vacuity Results
• Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
• Tools and Algorithms for the Construction and Analysis of Systems
• Relative liveness and behavior abstraction (extended abstract)
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Bounded model checking using satisfiability solving
• Model checking of safety properties

This page was built for publication: On relative and probabilistic finite counterability