Publication:5692280

From MaRDI portal


zbMath1070.68524MaRDI QIDQ5692280

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

Publication date: 28 September 2005



68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

68Q60: Specification and verification (program logics, model checking, etc.)


Related Items

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