Model checking of safety properties
From MaRDI portal
Publication:5949490
DOI10.1023/A:1011254632723zbMath0995.68061OpenAlexW1540883472WikidataQ64410838 ScholiaQ64410838MaRDI QIDQ5949490
Orna Kupferman, Moshe Y. Vardi
Publication date: 4 April 2002
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1011254632723
Related Items (57)
Foundations of fine-grained explainability ⋮ Spanning the spectrum from safety to liveness ⋮ Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective ⋮ Certifying DFA bounds for recognition and separation ⋮ GSTE is partitioned model checking ⋮ A brief account of runtime verification ⋮ Decentralised LTL monitoring ⋮ An extended framework for passive asynchronous testing ⋮ Similarity quantification for linear stochastic systems: a coupling compensator approach ⋮ Time window temporal logic ⋮ Model-Checking Linear-Time Properties of Quantum Systems ⋮ Temporal logic model predictive control ⋮ Monitoring first-order interval logic ⋮ Sound concurrent traces for online monitoring ⋮ On monitoring linear temporal properties ⋮ Deciding safety and liveness in TPTL ⋮ Quantitative safety and liveness ⋮ Compositional abstraction refinement for control synthesis ⋮ From LTL to rLTL monitoring: improved monitorability through robust semantics ⋮ Towards a grand unification of Büchi complementation constructions ⋮ A first-order logic characterization of safety and co-safety languages ⋮ Certified reinforcement learning with logic guidance ⋮ Formal methods to comply with rules of the road in autonomous driving: state of the art and grand challenges ⋮ On almost-sure intention deception planning that exploits imperfect observers ⋮ A first-order logic characterisation of safety and co-safety languages ⋮ Model-based reinforcement learning for approximate optimal control with temporal logic specifications ⋮ SySCoRe: Synthesis via Stochastic Coupling Relations ⋮ Optimized temporal monitors for SystemcC ⋮ Backdoors for linear temporal logic ⋮ Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited ⋮ First-order temporal logic monitoring with BDDs ⋮ Unbeast: Symbolic Bounded Synthesis ⋮ On relative and probabilistic finite counterability ⋮ Computer says no: verdict explainability for runtime monitors using a local proof system ⋮ Unnamed Item ⋮ Time-constrained temporal logic control of multi-affine systems ⋮ Symbolic approximate time-optimal control ⋮ On High-Quality Synthesis ⋮ Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption ⋮ Reverse Engineering Through Automata Learning ⋮ Congruence Relations for Büchi Automata ⋮ An Operational Guide to Monitorability ⋮ Compositional construction of infinite abstractions for networks of stochastic control systems ⋮ Model checking of linear-time properties in multi-valued systems ⋮ Streamable Fragments of Forward XPath ⋮ Automata-Theoretic Model Checking Revisited ⋮ Falsification of LTL Safety Properties in Hybrid Systems ⋮ Model Checking-Based Genetic Programming with an Application to Mutual Exclusion ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Reactive synthesis with maximum realizability of linear temporal logic specifications ⋮ A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring ⋮ CONTROLLABILITY AND COOPERATIVENESS ANALYSIS FOR AUTOMATIC ABSTRACTION REFINEMENT ⋮ From complementation to certification ⋮ Automated verification and synthesis of stochastic hybrid systems: a survey ⋮ Early nested word automata for XPath query answering on XML streams ⋮ Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
This page was built for publication: Model checking of safety properties
