scientific article; zbMATH DE number 5585443

zbMATH Open1179.68076MaRDI QIDQ5322945FDOQ5322945

Publication date: 23 July 2009

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

fairness model checking liveness communicating systems

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
Checking Timed Büchi Automata Emptiness Using LU-Abstractions
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
Approximate Verification of the Symbolic Dynamics of Markov Chains
Symbolic Model Checking for Alternating Projection Temporal Logic
On the Complexity of Branching-Time Logics
A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus
Nominal Automata for Resource Usage Control
Title not available (Why is that?)
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
Strategy synthesis for multi-dimensional quantitative objectives
Decompositions of graphs based on a new graph product
Formal Dependability Modeling and Analysis: A Survey
Model-Checking Linear-Time Properties of Quantum Systems
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
Reachability in MDPs: Refining Convergence of Value Iteration
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
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
A Semantics for Every GSPN
Title not available (Why is that?)
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
Generate & Check Method for Verifying Transition Systems in CafeOBJ
Reachability in parametric interval Markov chains using constraints
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
Doomsday equilibria for omega-regular games
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
Approximating Markov Processes by Averaging
\(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
Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints
Simple Strategies in Multi-Objective MDPs
Title not available (Why is that?)
Title not available (Why is that?)
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
Robust control for signal temporal logic specifications using discrete average space robustness
Title not available (Why is that?)
Title not available (Why is that?)
Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations
Decomposition of quantum Markov chains and its applications
Non-deterministic weighted automata evaluated over Markov chains
Monitorability for the Hennessy-Milner logic with recursion
Alternating-time temporal logics with linear past
Temporal logic guided safe model-based reinforcement learning: a hybrid systems approach
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
An impossibility result in automata-theoretic reinforcement learning
Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems
Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains
A spectral property for concurrent systems and some probabilistic applications
A novel learning algorithm for Büchi automata based on family of DFAs and classification trees
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
Title not available (Why is that?)
Encoding safety in \(\mathrm{CLL}_R\)
Sampling polynomial trajectories for LTL verification

Uses Software

Uppaal

   Recommendations

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)