scientific article; zbMATH DE number 5585443

Publication date: 23 July 2009

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

fairness liveness model checking communicating systems

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) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (only showing first 100 items - show all)

Which XML schemas are streaming bounded repairable? ⋮ What is decidable about partially observable Markov decision processes with \(\omega\)-regular objectives ⋮ Subject-oriented spatial logic ⋮ Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey ⋮ Measuring the constrained reachability in quantum Markov chains ⋮ Topological abstraction of higher-dimensional automata ⋮ Formal analysis of the kinematic Jacobian in screw theory ⋮ Bounded situation calculus action theories ⋮ Completeness and decidability results for CTL in constructive type theory ⋮ Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability ⋮ Formal abstraction and synthesis of parametric stochastic processes ⋮ Tweaking the odds in probabilistic timed automata ⋮ Adapting behaviors via reactive synthesis ⋮ Runtime monitors for Markov decision processes ⋮ Model checking finite-horizon Markov chains with probabilistic inference ⋮ Enforcing almost-sure reachability in POMDPs ⋮ Multi-agent planning under local LTL specifications and event-based synchronization ⋮ Reachability analysis of quantum Markov decision processes ⋮ Synthesizing efficient systems in probabilistic environments ⋮ Stubborn versus structural reductions for Petri nets ⋮ Parameterized model checking of rendezvous systems ⋮ Progression and verification of situation calculus agents with bounded beliefs ⋮ Finite abstractions with robustness margins for temporal logic-based control synthesis ⋮ ASM-based formal design of an adaptivity component for a cloud system ⋮ Interleaving isotactics -- an equivalence notion on behaviour abstractions ⋮ When are stochastic transition systems tameable? ⋮ Stability analysis and stabilization of stochastic linear impulsive, switched and sampled-data systems under dwell-time constraints ⋮ Formal modeling and verification for MVB ⋮ Compositional probabilistic verification through multi-objective model checking ⋮ Abstract probabilistic automata ⋮ Characterization and computation of infinite-horizon specifications over Markov processes ⋮ Optimal bounds in parametric LTL games ⋮ Model checking quantum Markov chains ⋮ The ins and outs of first-order runtime verification ⋮ Temporal logic model predictive control ⋮ Application of static analyses for state-space reduction to the microcontroller binary code ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ On the semantics of strategy logic ⋮ An interface theory for service-oriented design ⋮ Combined model checking for temporal, probabilistic, and real-time logics ⋮ Courcelle's theorem -- a game-theoretic approach ⋮ Model checking computation tree logic over finite lattices ⋮ An SMT-based approach to satisfiability checking of MITL ⋮ On algebra of languages representable by vertex-labeled graphs ⋮ The sweep-line state space exploration method ⋮ K\(^{\ast}\): A heuristic search algorithm for finding the \(k\) shortest paths ⋮ Model checking the observational determinism security property using PROMELA and SPIN ⋮ Pointfree expression and calculation: From quantification to temporal logic ⋮ Graph operations on parity games and polynomial-time algorithms ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Moving in a network under random failures: a complexity analysis ⋮ Model checking probabilistic systems against pushdown specifications ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ SAT-solving in CSP trace refinement ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ Three-valued abstraction for probabilistic systems ⋮ Modal transition systems with weight intervals ⋮ Linear temporal logic symbolic model checking ⋮ Probabilistic model validation for uncertain nonlinear systems ⋮ Formal communication elimination and sequentialization equivalence proofs for distributed system models ⋮ Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited ⋮ Practical algorithms for MSO model-checking on tree-decomposable graphs ⋮ Runtime verification of embedded real-time systems ⋮ Bounded semantics ⋮ Parameter synthesis for hierarchical concurrent real-time systems ⋮ Architecture-based resilience evaluation for self-adaptive systems ⋮ Development of global specification for dynamically adaptive software ⋮ Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties ⋮ Applications of an expressive statistical model checking approach to the analysis of genetic circuits ⋮ Confluence reduction for Markov automata ⋮ Scalable offline monitoring of temporal specifications ⋮ Organising LTL monitors over distributed systems with a global clock ⋮ A formal verification technique for behavioural model-to-model transformations ⋮ Model-based testing of probabilistic systems ⋮ Quantitative model-checking of controlled discrete-time Markov processes ⋮ The modeling library of eavesdropping methods in quantum cryptography protocols by model checking ⋮ Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components ⋮ Dynamic Bayesian networks for formal verification of structured stochastic processes ⋮ Nash equilibria in symmetric graph games with partial observation ⋮ Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games ⋮ Doomsday equilibria for omega-regular games ⋮ Computation tree logic model checking based on possibility measures ⋮ Model checking fuzzy computation tree logic ⋮ A temporal logic for micro- and macro-step-based real-time systems: foundations and applications ⋮ Performability assessment by model checking of Markov reward models ⋮ A linear translation from CTL\(^*\) to the first-order modal \(\mu \)-calculus ⋮ Automata-based axiom pinpointing ⋮ Encapsulating deontic and branching time specifications ⋮ Stochastic game logic ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ A formal semantics of extended hierarchical state transition matrices using CSP\# ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria ⋮ Probabilistic model checking of biological systems with uncertain kinetic rates ⋮ Developing topology discovery in Event-B ⋮ Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation ⋮ An efficient simulation algorithm based on abstract interpretation ⋮ 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

Uses Software

Uppaal

This page was built for publication: