Unfoldings: A partial-order approach to model checking.

From MaRDI portal
Publication:2426635


zbMath1153.68035MaRDI QIDQ2426635

Keijo Heljanko, Javier Esparza

Publication date: 23 April 2008

Published in: Monographs in Theoretical Computer Science. An EATCS Series (Search for Journal in Brave)


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

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68-02: Research exposition (monographs, survey articles) pertaining to computer science


Related Items

Unnamed Item, Unfolding Symbolic Attributed Graph Grammars, Non-interference by Unfolding, Construction and SAT-Based Verification of Contextual Unfoldings, Unnamed Item, Unnamed Item, High-level representation of benchmark families for Petri games, Concurrency in Boolean networks, A combinatorial study of async/await processes, Unfolding-based dynamic partial order reduction of asynchronous distributed programs, Reasoning about equilibria in game-like concurrent systems, Recent advances in unfolding technique, Modular discrete time approximations of distributed hybrid automata, Exploiting step semantics for efficient bounded model checking of asynchronous systems, Efficient unfolding of contextual Petri nets, Program verification: state of the art, problems, and results. II, On a homomorphism of a component Petri net, Petri games: synthesis of distributed systems with causal memory, Model-checking games for fixpoint logics with partial order models, Petri nets for modelling metabolic pathways: a survey, Untanglings: a novel approach to analyzing concurrent systems, A Nice labelling for tree-like event structures of degree 3, Compact and efficiently verifiable models for concurrent systems, Multilevel transitive and intransitive non-interference, causally, Petri nets are dioids: a new algebraic foundation for non-deterministic net theory, Star-topology decoupled state space search, Quasi-optimal partial order reduction, Pomset bisimulation and unfolding for reset Petri nets, Canonical representations for direct generation of strategies in high-level Petri games, Solving high-level Petri games, Distributed computation of vector clocks in Petri net unfoldings for test selection, Symbolic unfolding of parametric stopwatch Petri nets, Independence Abstractions and Models of Concurrency, Succinct discrete time approximations of distributed hybrid automata, Accurate hybridization of nonlinear systems, Compositional analysis for linear control systems, On integration of event-based estimation and robust MPC in a feedback loop, From synchronous programs to symbolic representations of hybrid systems, A descent algorithm for the optimal control of constrained nonlinear switched dynamical systems, Timed automata with observers under energy constraints, Real-time scheduling of mixture-of-experts systems with limited resources, On a control algorithm for time-varying processor availability, Timed I/O automata, Receding horizon control for temporal logic specifications, Synthesis using approximately bisimilar abstractions, Oscillation analysis of linearly coupled piecewise affine systems, On infinity norms as Lyapunov functions for piecewise affine systems, Identifiability of discrete-time linear switched systems, Rank properties of poincare maps for hybrid systems with applications to bipedal walking, Stealthy deception attacks on water SCADA systems, Comparison of overapproximation methods for stability analysis of networked control systems, Distributed Kalman Filter algorithms for self-localization of mobile devices, Convergence results for ant routing algorithms viastochastic approximation, Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems, Automatic invariant generation for hybrid systems using ideal fixed points, Safe compositional network sketches, Bayesian statistical model checking with application to Simulink/Stateflow verification, On the connections between PCTL and dynamic programming, Modeling and verification of stochastic hybrid systems using HIOA, A generating function approach to the stability of discrete-time switched linear systems, Stabilization of planar switched linear systems using polar coordinates, Amir Pnueli and the dawn of hybrid systems, Local Model Checking in a Logic for True Concurrency, Occurrence Nets Then and Now: The Path to Structured Occurrence Nets, An Algorithm for Direct Construction of Complete Merged Processes, Efficient Contextual Unfolding, Performance Evaluation of Schedulers in a Probabilistic Setting, Partial-Order Reduction, Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems, Model Checking Data Flows in Concurrent Network Updates, Oclets – Scenario-Based Modeling with Petri Nets


Uses Software