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)
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 (71)
Compact and efficiently verifiable models for concurrent systems ⋮ Performance Evaluation of Schedulers in a Probabilistic Setting ⋮ Partial-Order Reduction ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ Petri nets for modelling metabolic pathways: a survey ⋮ Multilevel transitive and intransitive non-interference, causally ⋮ Solving high-level Petri games ⋮ Unfolding Symbolic Attributed Graph Grammars ⋮ High-level representation of benchmark families for Petri games ⋮ Recent advances in unfolding technique ⋮ Concurrency in Boolean networks ⋮ Modular discrete time approximations of distributed hybrid automata ⋮ A combinatorial study of async/await processes ⋮ Distributed computation of vector clocks in Petri net unfoldings for test selection ⋮ Independence Abstractions and Models of Concurrency ⋮ Unnamed Item ⋮ Untanglings: a novel approach to analyzing concurrent systems ⋮ Unfolding-based dynamic partial order reduction of asynchronous distributed programs ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ Efficient unfolding of contextual Petri nets ⋮ Petri nets are dioids: a new algebraic foundation for non-deterministic net theory ⋮ Unnamed Item ⋮ 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 ⋮ Program verification: state of the art, problems, and results. II ⋮ On a homomorphism of a component Petri net ⋮ Local Model Checking in a Logic for True Concurrency ⋮ Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems ⋮ Model Checking Data Flows in Concurrent Network Updates ⋮ Occurrence Nets Then and Now: The Path to Structured Occurrence Nets ⋮ An Algorithm for Direct Construction of Complete Merged Processes ⋮ Star-topology decoupled state space search ⋮ Petri games: synthesis of distributed systems with causal memory ⋮ Symbolic unfolding of parametric stopwatch Petri nets ⋮ Non-interference by Unfolding ⋮ Model-checking games for fixpoint logics with partial order models ⋮ A Nice labelling for tree-like event structures of degree 3 ⋮ Construction and SAT-Based Verification of Contextual Unfoldings ⋮ Unnamed Item ⋮ Quasi-optimal partial order reduction ⋮ Efficient Contextual Unfolding ⋮ Oclets – Scenario-Based Modeling with Petri Nets ⋮ Pomset bisimulation and unfolding for reset Petri nets ⋮ Canonical representations for direct generation of strategies in high-level Petri games
Uses Software
This page was built for publication: Unfoldings: A partial-order approach to model checking.
