scientific article; zbMATH DE number 5585443
From MaRDI portal
Publication:5322945
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) 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)- The complexity of computing a bisimilarity pseudometric on probabilistic automata
- Non-deterministic Weighted Automata on Random Words
- Optimal bounds in parametric LTL games
- Model checking quantum Markov chains
- Team semantics for the specification and verification of hyperproperties
- Least-violating control strategy synthesis with safety rules
- An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
- Subject-oriented spatial logic
- Fair termination for parameterized probabilistic concurrent systems
- Measuring the constrained reachability in quantum Markov chains
- Computation tree logic model checking based on multi-valued possibility measures
- Bisimulations of probabilistic Boolean networks
- Model checking probabilistic systems against pushdown specifications
- Learning nonlinear hybrid systems: from sparse optimization to support vector regression
- A Markovian model for the spread of the SARS-CoV-2 virus
- Three-valued abstraction for probabilistic systems
- A deductive approach towards reasoning about algebraic transition systems
- Computing probabilistic bisimilarity distances for probabilistic automata
- Specifying reversibility with \(\mathrm{TLA}^+\)
- Equivalence checking of Petri net models of programs using static and dynamic cut-points
- Flowpipe approximation and clustering in space-time
- Optimal control of multi-task Boolean control networks via temporal logic
- \(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
- Geometric Model Checking of Continuous Space
- Verify heaps via unified model checking
- Nash equilibrium and bisimulation invariance
- Book review of: E. M. Clarke (ed.) et al., Handbook of model checking
- Practical algorithms for MSO model-checking on tree-decomposable graphs
- To compose, or not to compose, that is the question: an analysis of compositional state space generation
- Observer design for a class of piecewise affine hybrid systems
- Tracking differentiable trajectories across polyhedra boundaries
- On probabilistic monitorability
- Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
- Solving odd-fair parity games
- Reachability games and friends: a journey through the Lens of memory and complexity (invited talk)
- Linear dynamical systems with continuous weight functions
- Learning-based symbolic abstractions for nonlinear control systems
- Beyond series-parallel concurrent systems: the case of arch processes
- From Iteration to System Failure: Characterizing the FITness of Periodic Weakly-Hard Systems
- Model-Free Reinforcement Learning for Stochastic Parity Games
- Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States
- Reaching Your Goal Optimally by Playing at Random with No Memory
- Data-driven abstraction-based control synthesis
- Skolem and positivity completeness of ergodic Markov chains
- Robust satisfaction of metric interval temporal logic objectives in adversarial environments
- scientific article; zbMATH DE number 7455747 (Why is no real title available?)
- Probabilistic model checking for energy-utility analysis
- Minimal counterexamples for linear-time probabilistic verification
- scientific article; zbMATH DE number 7561726 (Why is no real title available?)
- Quantifying masking fault-tolerance via fair stochastic games
- Formal Verification for Components and Connectors
- A formal verification technique for behavioural model-to-model transformations
- Model-based testing of probabilistic systems
- K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
- Simulation for lattice-valued doubly labeled transition systems
- Complexity of model checking MDPs against LTL specifications
- scientific article; zbMATH DE number 7559393 (Why is no real title available?)
- scientific article; zbMATH DE number 7561612 (Why is no real title available?)
- Projection for Büchi Tree Automata with Constraints between Siblings
- Modal transition systems with weight intervals
- Abstraction-based synthesis for stochastic systems with omega-regular objectives
- scientific article; zbMATH DE number 7649916 (Why is no real title available?)
- A framework for compositional nonblocking verification of extended finite-state machines
- \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
- Limited-information control of hybrid systems via reachable set propagation
- A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
- Of cores: a partial-exploration framework for Markov decision processes
- Specification and verification of multi-clock systems using a temporal logic with clock constraints
- scientific article; zbMATH DE number 438994 (Why is no real title available?)
- 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
- Comparison of algorithms for simple stochastic games
- Local higher-order fixpoint iteration
- Model checking hyperproperties for Markov decision processes
- Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies
- Time-bounded termination analysis for probabilistic programs with delays
- Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability
- Formal abstraction and synthesis of parametric stochastic processes
- Adapting behaviors via reactive synthesis
- Enforcing almost-sure reachability in POMDPs
- Model checking finite-horizon Markov chains with probabilistic inference
- Tweaking the odds in probabilistic timed automata
- Runtime monitors for Markov decision processes
- Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Playing Against Fair Adversaries in Stochastic Games with Total Rewards
- Markovian imprecise jump processes: extension to measurable variables, convergence theorems and algorithms
- Model checking of pushdown systems for projection temporal logic
- Compositional design of stochastic timed automata
- Comparison of algorithms for simple stochastic games
- Fixpoint Theory -- Upside Down
- Sound approximate and asymptotic probabilistic bisimulations for PCTL
- LTL model checking of time-inhomogeneous Markov chains
- Analyzing oscillatory behavior with formal methods
- A theory for the semantics of stochastic and non-deterministic continuous systems
- Compositional failure detection in structured transition systems
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)
