Model checking of safety properties
From MaRDI portal
Recommendations
Cited in
(92)- Spanning the spectrum from safety to liveness
- Compositional abstraction refinement for control synthesis
- Safety property-driven stubborn sets
- Backdoors for linear temporal logic
- On relative and probabilistic finite counterability
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
- Certifying DFA bounds for recognition and separation
- Similarity quantification for linear stochastic systems: a coupling compensator approach
- First-order temporal logic monitoring with BDDs
- Time-constrained temporal logic control of multi-affine systems
- Compositional construction of infinite abstractions for networks of stochastic control systems
- Model checking of linear-time properties in multi-valued systems
- 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
- Early nested word automata for XPath query answering on XML streams
- GSTE is partitioned model checking
- A brief account of runtime verification
- Time window temporal logic
- Optimized temporal monitors for SystemcC
- From complementation to certification
- Property directed abstract interpretation
- Bounded model checking for timed automata
- Model-checking linear-time properties of quantum systems
- Unbeast: Symbolic Bounded Synthesis
- An extended framework for passive asynchronous testing
- On the Construction of Fine Automata for Safety Properties
- Falsification of LTL Safety Properties in Hybrid Systems
- Deciding safety and liveness in TPTL
- scientific article; zbMATH DE number 1982198 (Why is no real title available?)
- Modeling and Verification of High-Assurance Properties of Safety-Critical Systems
- Model Checking Safety-Critical Systems Using Safecharts
- Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
- scientific article; zbMATH DE number 2102704 (Why is no real title available?)
- Finite Models vs Tree Automata in Safety Verification
- Streamable fragments of forward XPath
- Symbolic approximate time-optimal control
- Streamability of nested word transductions
- scientific article; zbMATH DE number 7056237 (Why is no real title available?)
- On Locally Checkable Properties
- Automata-Theoretic Model Checking Revisited
- Model Checking-Based Genetic Programming with an Application to Mutual Exclusion
- CONTROLLABILITY AND COOPERATIVENESS ANALYSIS FOR AUTOMATIC ABSTRACTION REFINEMENT
- On high-quality synthesis
- Monitoring first-order interval logic
- Sound concurrent traces for online monitoring
- On monitoring linear temporal properties
- Quantitative safety and liveness
- 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
- 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
- Incremental dead state detection in logarithmic time
- Prenex universal first-order safety properties
- A mobile robot controller using reinforcement learning under scLTL specifications with uncertainties
- Efficient reactive synthesis using mode decomposition
- Towards the exact complexity of realizability for safety LTL
- Symbolic solution of Emerson-Lei games for reactive synthesis
- Succinctness of cosafety fragments of LTL via combinatorial proof systems
- Towards an efficient implementation of a tableau method for reactive safety specifications
- On the power of automata minimization in reactive synthesis
- Expressiveness of extended bounded response \textsf{LTL}
- The best a monitor can do
- Asynchronous composition of LTL properties over infinite and finite traces
- Monotonicity characterizations of regular languages
- Secondary safety control for systems with sector bounded nonlinearities
- Automatic WSTS-based repair and deadlock detection of parameterized systems
- SySCcoRe 2.0: toolset for formal control synthesis of continuous-state stochastic systems and temporal logic specifications
- Semantics for linear-time temporal logic with finite observations
- Monotonicity characterizations of regular languages
- Safety and liveness of quantitative automata
- Safety and liveness of quantitative properties and automata
- Context-triggered games for reactive synthesis over stochastic systems via control barrier certificates
- Memoryless concretization relation
- A theory of fine-grained lineage for functions on structured objects
- \( \textsc{ltl}_f\) synthesis under environment specifications for reachability and safety properties
- Efficient strategy synthesis for switched stochastic systems with distributional uncertainty
- On robust supervisory control of metric discrete event systems for scLTL specifications
- An optimal pastification algorithm for \(\mathsf{LTL} \lbrack \mathsf{X}, \mathsf{F} \rbrack\) and \(\mathsf{LTL} \lbrack \mathsf{X}, \mathsf{G} \rbrack \)
- Foundations of fine-grained explainability
- Prognosis of \(\omega\)-languages for the diagnosis of *-languages: a topological perspective
- Temporal logic model predictive control
This page was built for publication: Model checking of safety properties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5949490)
