Compositional State Space Reduction Using Untangled Actions

We propose a compositional technique for efficient verification of networks of parallel processes. It is based on an automatic analysis of LTSs of individual processes (using a failure-based equivalence which preserves divergences) that determines their sets of “conflict-free” actions, called untangled actions. Untangled actions are compositional, i.e. synchronisation on untangled actions will not destroy their “conflict-freedom”. For networks of processes, using global untangled actions derived from local ones, efficient reduction algorithms have been devised for systems with a large number of small processes running in parallel.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Xu Wang, Marta Z. Kwiatkowska
• Keywords: Compositional Technique, ENTCS 2007, Global Untangled Actions, Untangled Actions