scientific article; zbMATH DE number 5585443
From MaRDI portal
Publication:5322945
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
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)
- Simulation for lattice-valued doubly labeled transition systems
- A formal verification technique for behavioural model-to-model transformations
- Model-based testing of probabilistic systems
- A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
- Probabilistic verification of Herman's self-stabilisation algorithm
- The complexity of reachability in parametric Markov decision processes
- Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems
- A semantics for every GSPN
- Model-checking linear-time properties of quantum systems
- Formal dependability modeling and analysis: a survey
- On the Complexity of Branching-Time Logics
- A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus
- Reachability in MDPs: refining convergence of value iteration
- Generate \& check method for verifying transition systems in CafeOBJ
- Approximating Markov processes by averaging
- Weighted linear dynamic logic
- Title not available (Why is that?)
- Moving in a network under random failures: a complexity analysis
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- SAT-solving in CSP trace refinement
- Title not available (Why is that?)
- A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time
- Control design for specifications on stochastic hybrid systems
- Iterative temporal motion planning for hybrid systems in partially unknown environments
- Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets
- Decompositions of graphs based on a new graph product
- Automated verification and synthesis of stochastic hybrid systems: a survey
- Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems
- Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
- Application of static analyses for state-space reduction to the microcontroller binary code
- On the decidability of stability of hybrid systems
- An efficient simulation algorithm based on abstract interpretation
- Linear temporal logic symbolic model checking
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited
- Automated Verification of Signalling Principles in Railway Interlocking Systems
- Automata-based axiom pinpointing
- Runtime verification of embedded real-time systems
- Bounded semantics
- Architecture-based resilience evaluation for self-adaptive systems
- Development of global specification for dynamically adaptive software
- Pointfree expression and calculation: From quantification to temporal logic
- Checking timed Büchi automata emptiness using LU-abstractions
- Opacity for linear constraint Markov chains
- Correctness kernels of abstract interpretations
- Applications of an expressive statistical model checking approach to the analysis of genetic circuits
- Symbolic model checking for alternating projection temporal logic
- Probabilistic model checking of biological systems with uncertain kinetic rates
- Confluence reduction for Markov automata
- Parallel decomposition and concurrent satisfaction for heterogeneous multi-robot task and motion planning under temporal logic specifications
- Approximate verification of the symbolic dynamics of Markov chains
- Quantitative model-checking of controlled discrete-time Markov processes
- Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components
- The modeling library of eavesdropping methods in quantum cryptography protocols by model checking
- Nominal automata for resource usage control
- Organising LTL monitors over distributed systems with a global clock
- Scalable offline monitoring of temporal specifications
- Dynamic Bayesian networks for formal verification of structured stochastic processes
- Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games
- Nash equilibria in symmetric graph games with partial observation
- Computation tree logic model checking based on possibility measures
- Model checking fuzzy computation tree 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
- Verify heaps via unified model checking
- Formal Verification for Components and Connectors
- On subgame perfect equilibria in turn-based reachability timed games
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Probabilistic causes in Markov chains
- Decidability of approximate Skolem problem and applications to logical verification of dynamical properties of Markov chains
- Decomposition of quantum Markov chains and its applications
- Non-deterministic weighted automata evaluated over Markov chains
- Monitorability for the Hennessy-Milner logic with recursion
- Results on alternating-time temporal logics with linear past
- Alternating-time temporal logics with linear past
- Temporal logic guided safe model-based reinforcement learning: a hybrid systems approach
- Farkas certificates and minimal witnesses for probabilistic reachability constraints
- Approximate partial order reduction
- IPL: an integration property language for multi-model cyber-physical systems
- Producing explanations for rich logics
- Automated formal analysis and verification: an overview
- Model checking reconfigurable Petri nets with Maude
- An impossibility result in automata-theoretic reinforcement learning
- Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems
- A spectral property for concurrent systems and some probabilistic applications
- Probabilistic model checking of labelled Markov processes via finite approximate bisimulations
- A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
- Probabilistic logics based on Riesz spaces
- Are parametric Markov chains monotonic?
- Sequential convex programming for the efficient verification of parametric MDPs
- Simple strategies in multi-objective MDPs
- Game-based local model checking for the coalgebraic \(\mu\)-calculus
- Distributed synthesis for parameterized temporal logics
- Data-driven modelling and probabilistic analysis of interactive software usage
- The quest for minimal quotients for probabilistic and Markov automata
- On the metric-based approximate minimization of Markov chains
- Static and dynamic property-preserving updates
- Fluid model checking of timed properties
- Algorithms to compute probabilistic bisimilarity distances for labelled Markov chains
Uses Software
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)
