scientific article; zbMATH DE number 5585443

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

scientific article; zbMATH DE number 1487860
Model Checking: From Tools to Theory
scientific article; zbMATH DE number 438994
scientific article; zbMATH DE number 2080188
A proof theory for model checking: an extended abstract
scientific article; zbMATH DE number 1746645
Handbook of model checking
Introduction to model checking
A proof theory for model checking

Cited in

(only showing first 100 items - show all)

Developing topology discovery in Event-B
An efficient simulation algorithm based on abstract interpretation
Formal analysis of the kinematic Jacobian in screw theory
Reachability analysis of quantum Markov decision processes
Stubborn versus structural reductions for Petri nets
Parameterized model checking of rendezvous systems
Interleaving isotactics -- an equivalence notion on behaviour abstractions
When are stochastic transition systems tameable?
On clock-aware LTL parameter synthesis of timed automata
A deductive approach towards reasoning about algebraic transition systems
Reformulation of the linear program for completely ergodic MDPs with average cost criteria
Symbolic control design for monotone systems with directed specifications
On partial state matching
Model checking the evolution of gene regulatory networks
Simulation relations for fault-tolerance
Learning deterministic probabilistic automata from a model checking perspective
Compositional abstraction refinement for control synthesis
Augmented finite transition systems as abstractions for control synthesis
Towards scalable synthesis of stochastic control systems
Quantitative model checking of linear-time properties based on generalized possibility measures
Markov chains and Markov decision processes in Isabelle/HOL
From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
Abstract model repair for probabilistic systems
First-order -calculus over generic transition systems and applications to the situation calculus
Decentralized abstractions for multi-agent systems under coupled constraints
Symbolic checking of fuzzy CTL on fuzzy program graph
Probabilistic verification of hierarchical leader election protocol in dynamic systems
Verification of asynchronous systems with an unspecified component
Verification and control for probabilistic hybrid automata with finite bisimulations
Decompositions of graphs based on a new graph product
Robust control for signal temporal logic specifications using discrete average space robustness
Opacity for linear constraint Markov chains
Decomposition of quantum Markov chains and its applications
The quest for minimal quotients for probabilistic and Markov automata
Model checking Markov population models by stochastic approximations
Distributed synthesis for parameterized temporal logics
On the metric-based approximate minimization of Markov chains
Data-driven modelling and probabilistic analysis of interactive software usage
Stabilization and control Lyapunov functions for language constrained discrete-time switched linear systems
Guaranteed model-based fault detection in cyber-physical systems: a model invalidation approach
A study on shuffle, stopwatches and independently evolving clocks
A formal approach to adaptive software: continuous assurance of non-functional requirements
Probabilistic verification of Herman's self-stabilisation algorithm
TASS: the toolkit for accurate scientific software
\(L^\ast\)-based learning of Markov decision processes (extended version)
Counterexample-guided inductive synthesis for probabilistic systems
RiskStructures: a design algebra for risk-aware machines
Verify heaps via unified model checking
Alternating-time temporal logics with linear past
Intention as commitment toward time
Deep reinforcement learning with temporal logics
On subgame perfect equilibria in turn-based reachability timed games
Computer says no: verdict explainability for runtime monitors using a local proof system
Probabilistic black-box reachability checking (extended version)
Non-deterministic weighted automata evaluated over Markov chains
Ensuring liveness properties of distributed systems: open problems
Producing explanations for rich logics
IPL: an integration property language for multi-model cyber-physical systems
To compose, or not to compose, that is the question: an analysis of compositional state space generation
Compositional reasoning for shared-variable concurrent programs
Approximate partial order reduction
UNITY and Büchi automata
Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems
Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
A spectral property for concurrent systems and some probabilistic applications
Static and dynamic property-preserving updates
Finding provably optimal Markov chains
A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
Encoding safety in \(\mathrm{CLL}_R\)
Sampling polynomial trajectories for LTL verification
Decoy allocation games on graphs with temporal logic objectives
Funnel control for fully actuated systems under a fragment of signal temporal logic specifications
Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations
Logic for \(\omega\)-pushdown automata
Enhancing probabilistic model checking with ontologies
TOrPEDO : witnessing model correctness with topological proofs
Statistical model checking for variability-intensive systems: applications to bug detection and minimization
Moment-based analysis of Bayesian network properties
Symbolic models for infinite networks of control systems: a compositional approach
Safe-visor architecture for sandboxing (AI-based) unverified controllers in stochastic cyber-physical systems
Diagnosability verification using LTL model checking
Compositional construction of control barrier functions for continuous-time stochastic hybrid systems
Robust approximate symbolic models for a class of continuous-time uncertain nonlinear systems via a control interface
An algebraic method to fidelity-based model checking over quantum Markov chains
Computation tree logic model checking over possibilistic decision processes under finite-memory scheduler
Risk verification of stochastic systems with neural network controllers
Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models
Bounds for synchronizing Markov decision processes
Automated verification and synthesis of stochastic hybrid systems: a survey
Learning-based symbolic abstractions for nonlinear control systems
Lifted model checking for relational MDPs
Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations
A game-theoretic approach for the synthesis of complex systems
CTL* model checking for data-aware dynamic systems with arithmetic
Decisiveness of stochastic systems and its application to hybrid models
Comparison of algorithms for simple stochastic games
Model checking hyperproperties for Markov decision processes
Local higher-order fixpoint iteration
Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies
Robustly complete finite-state abstractions for verification of stochastic systems

Describes a project that uses

Uses Software

Uppaal

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5322945)