scientific article; zbMATH DE number 2209335

Moshe Y. Vardi, Orna Kupferman, Rajeev Alur, Thomas A. Henzinger

Publication date: 28 September 2005

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

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Abstraction in Fixpoint Logic ⋮ Combining Partial Specifications using Alternating Interface Automata ⋮ An Algorithm for Probabilistic Alternating Simulation ⋮ An abstraction-refinement methodology for reasoning about network games ⋮ Generalized interface automata with multicast synchronization ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Finite abstractions with robustness margins for temporal logic-based control synthesis ⋮ A Pre-congruence Format for XY-simulation ⋮ Synthesising succinct strategies in safety games with an application to real-time scheduling ⋮ A logic for conditional local strategic reasoning ⋮ Unnamed Item ⋮ Formal controller synthesis from specifications given by discrete-time hybrid automata ⋮ Symbolic control design for monotone systems with directed specifications ⋮ A game-theoretic approach to fault diagnosis and identification of hybrid systems ⋮ The refinement calculus of reactive systems ⋮ Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement ⋮ An algebraic theory of interface automata ⋮ From interface automata to hypercontracts ⋮ A Simpler Alternative: Minimizing Transition Systems Modulo Alternating Simulation Equivalence ⋮ Augmenting ATL with strategy contexts ⋮ A survey of stochastic \(\omega \)-regular games ⋮ Robust stutter bisimulation for abstraction and controller synthesis with disturbance ⋮ Goodbye ioco ⋮ Modal event-clock specifications for timed component-based design ⋮ Automated temporal equilibrium analysis: verification and synthesis of multi-player games ⋮ Unnamed Item ⋮ Antichains and compositional algorithms for LTL synthesis ⋮ Specifications for decidable hybrid games ⋮ Refinement modal logic ⋮ Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol ⋮ Interface simulation distances ⋮ Deadlock-free output feedback controller design based on approximately abstracted observers ⋮ A modal characterization of alternating approximate bisimilarity ⋮ Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata ⋮ Symbolic models for nonlinear control systems affected by disturbances ⋮ Deductive verification of alternating systems ⋮ Conditions of contracts for separating responsibilities in heterogeneous systems ⋮ Refining autonomous agents with declarative beliefs and desires ⋮ Quantitative fair simulation games ⋮ Refining strategic ability in alternating-time temporal logic ⋮ Interface synthesis and protocol conversion ⋮ Model-Based Testing ⋮ Quantitative Simulation Games ⋮ Composing model programs for analysis ⋮ A game approach to determinize timed automata ⋮ On timed alternating simulation for concurrent timed games ⋮ Unnamed Item ⋮ Test generation from state based use case models ⋮ Error-pruning in interface automata ⋮ Controller synthesis for bisimulation equivalence ⋮ Unnamed Item ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ Simulation distances ⋮ Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation ⋮ Refinement checking on parametric modal transition systems ⋮ Play to Test