scientific article; zbMATH DE number 5585443

zbMATH Open1179.68076MaRDI QIDQ5322945FDOQ5322945

Authors: Christel Baier, Joost-Pieter Katoen 

Publication date: 23 July 2009

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

fairnessmodel checkinglivenesscommunicating systems

Mathematics Subject Classification ID

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)

Cited In (only showing first 100 items - show all)

• Optimal bounds in parametric LTL games
• Model checking quantum Markov chains
• Model checking probabilistic systems against pushdown specifications
• Three-valued abstraction for probabilistic systems
• Practical algorithms for MSO model-checking on tree-decomposable graphs
• Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
• Limited-information control of hybrid systems via reachable set propagation
• Title not available (Why is that?)
• Minimal counterexamples for linear-time probabilistic verification
• K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths
• Modal transition systems with weight intervals
• 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
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• An interface theory for service-oriented design
• Combined model checking for temporal, probabilistic, and real-time logics
• Unfoldings: A partial-order approach to model checking.
• Which XML schemas are streaming bounded repairable?
• What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives
• Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey
• Courcelle's theorem -- a game-theoretic approach
• On algebra of languages representable by vertex-labeled graphs
• The sweep-line state space exploration method
• Topological abstraction of higher-dimensional automata
• Bounded situation calculus action theories
• Progression and verification of situation calculus agents with bounded beliefs
• An SMT-based approach to satisfiability checking of MITL
• Quantitative analysis under fairness constraints
• Bisimulations meet PCTL equivalences for probabilistic automata
• Reachability analysis of quantum Markov decision processes
• Completeness and decidability results for CTL in constructive type theory
• Graph operations on parity games and polynomial-time algorithms
• Multi-agent planning under local LTL specifications and event-based synchronization
• Symbolic execution of Reo circuits using constraint automata
• Synthesizing efficient systems in probabilistic environments
• Model checking \(\omega\)-regular properties for quantum Markov chains
• Model checking quantum systems. Principles and algorithms
• The ins and outs of first-order runtime verification
• Title not available (Why is that?)
• An algebraic method to fidelity-based model checking over quantum Markov chains
• Model checking QCTL plus on quantum Markov chains
• The 4C Spectrum of Fundamental Behavioral Relations for Concurrent Systems
• Analyzing probabilistic pushdown automata
• Finite abstractions with robustness margins for temporal logic-based control synthesis
• ASM-based formal design of an adaptivity component for a cloud system
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• Model checking linear-time properties of probabilistic systems
• Compositional probabilistic verification through multi-objective model checking
• A toolbox for simulation of hybrid systems in Matlab/Simulink. Hybrid Equations (HyEQ) Toolbox
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• On digraph width measures in parameterized algorithmics
• Controllability of probabilistic Boolean control networks based on transition probability matrices
• Probabilistic model validation for uncertain nonlinear systems
• Model checking the evolution of gene regulatory networks
• Synthesizing efficient controllers
• Stability analysis and stabilization of stochastic linear impulsive, switched and sampled-data systems under dwell-time constraints
• Parameter synthesis for hierarchical concurrent real-time systems
• Compositional verification of asynchronous concurrent systems using CADP
• Symbolic computation of differential equivalences
• First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus
• Computable fixpoints in well-structured symbolic model checking
• Formal modeling and verification for MVB
• On the formalization of cardinal points of optical systems
• Computing Behavioral Relations for Probabilistic Concurrent Systems
• Runtime verification using a temporal description logic
• Automatic verification of competitive stochastic systems
• Stability of shuffled switched linear systems: A joint spectral radius approach
• TASS: the toolkit for accurate scientific software
• Stabhyli -- a tool for automatic stability verification of non-linear hybrid systems
• Zélus: a synchronous language with ODEs
• Abstract probabilistic automata
• Characterization and computation of infinite-horizon specifications over Markov processes
• Probabilistic black-box reachability checking (extended version)
• Computation tree logic model checking based on multi-valued possibility measures
• Equivalence checking of Petri net models of programs using static and dynamic cut-points
• Optimal control of multi-task Boolean control networks via temporal logic
• Learning-based symbolic abstractions for nonlinear control systems
• Of cores: a partial-exploration framework for Markov decision processes
• Abstraction-based synthesis for stochastic systems with omega-regular objectives
• 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
• Comparison of algorithms for simple stochastic games
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems
• Life is random, time is not: Markov decision processes with window objectives
• Markovian imprecise jump processes: extension to measurable variables, convergence theorems and algorithms
• Efficient convex zone merging in parametric timed automata
• Model checking for entanglement swapping
• Data-driven verification of stochastic linear systems with signal temporal logic constraints
• Robustly complete finite-state abstractions for verification of stochastic systems
• Timed games with bounded window parity objectives
• Context-free timed formalisms: robust automata and linear temporal logics
• Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
• Safe schedulability of bounded-rate multi-mode systems

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)