An improvement of McMillan's unfolding algorithm

DOI10.1023/A:1014746130920zbMath1017.68085OpenAlexW2164024827MaRDI QIDQ1600655

Stefan Römer, Javier Esparza, Walter Vogler

Publication date: 16 June 2002

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1014746130920

zbMATH Keywords

finite-state Petri netsMcMillan's algorithm

Mathematics Subject Classification ID

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

Related Items (43)

Star-Topology Decoupling in SPIN ⋮ Unfolding of parametric Boolean networks ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ On the well-foundedness of adequate orders used for construction of complete unfolding prefixes ⋮ Merged processes: a new condensed representation of Petri net behaviour ⋮ What topology tells us about diagnosability in partial order semantics ⋮ Efficient semantics-based compliance checking using LTL formulae and unfolding ⋮ Verification of bounded Petri nets using integer programming ⋮ Process Mining Reloaded: Event Structures as a Unified Representation of Process Models and Event Logs ⋮ Multilevel transitive and intransitive non-interference, causally ⋮ Computing the reveals relation in occurrence nets ⋮ Recent advances in unfolding technique ⋮ Parameter space abstraction and unfolding semantics of discrete regulatory networks ⋮ Cut-off theorems for the \textit{PV}-model ⋮ Unfolding Graph Transformation Systems: Theory and Applications to Verification ⋮ The sweep-line state space exploration method ⋮ Untanglings: a novel approach to analyzing concurrent systems ⋮ Efficient unfolding of contextual Petri nets ⋮ Unnamed Item ⋮ A structural approach for the analysis of Petri Nets by reduced unfoldings ⋮ Verification of concurrent programs using Petri net unfoldings ⋮ Trellis processes: a compact representation for runs of concurrent systems ⋮ An Algorithm for Direct Construction of Complete Merged Processes ⋮ Spreading nets: a uniform approach to unfoldings ⋮ Star-topology decoupled state space search ⋮ Detection of temporal anomalies for partially observed timed PNs ⋮ Symbolic unfolding of parametric stopwatch Petri nets ⋮ QoS-aware management of monotonic service orchestrations ⋮ Flow Unfolding of Multi-clock Nets ⋮ Merging Relations: A Way to Compact Petri Nets’ Behaviors Uniformly ⋮ Directed Unfolding of Petri Nets ⋮ McMillan’s Complete Prefix for Contextual Nets ⋮ Unnamed Item ⋮ Construction and SAT-Based Verification of Contextual Unfoldings ⋮ Unnamed Item ⋮ A theory of structural stationarity in the \(\pi\)-calculus ⋮ Efficient Contextual Unfolding ⋮ Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics ⋮ STG decomposition strategies in combination with unfolding ⋮ Critical Paths in the Partial Order Unfolding of a Stochastic Petri Net ⋮ A Practical Approach to Verification of Mobile Systems Using Net Unfoldings ⋮ Pomset bisimulation and unfolding for reset Petri nets ⋮ Control of safe ordinary Petri nets using unfolding

This page was built for publication: An improvement of McMillan's unfolding algorithm