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)

• \(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
• Distributed PROMPT-LTL synthesis
• Title not available (Why is that?)
• An efficient algorithm for computing causal trace sets in causality checking
• Encoding safety in \(\mathrm{CLL}_R\)
• Sampling polynomial trajectories for LTL verification
• Decoy allocation games on graphs with temporal logic objectives
• Guaranteed model-based fault detection in cyber-physical systems: a model invalidation approach
• Stabilization and control Lyapunov functions for language constrained discrete-time switched linear systems
• Verification of multiplayer stochastic games via abstract dependency graphs
• A study on shuffle, stopwatches and independently evolving clocks
• A formal approach to adaptive software: continuous assurance of non-functional requirements
• Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations
• Funnel control for fully actuated systems under a fragment of signal temporal logic specifications
• Probabilistic total store ordering
• Title not available (Why is that?)
• Inferring Symbolic Automata
• Model-Checking Counting Temporal Logics on Flat Structures
• Certified reinforcement learning with logic guidance
• Non-deterministic Weighted Automata on Random Words
• On probabilistic monitorability
• 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

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)