Model checking of safety properties
From MaRDI portal
Publication:5949490
DOI10.1023/A:1011254632723zbMath0995.68061OpenAlexW1540883472MaRDI 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
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, 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
