Oxford logo
[WK06] X Wang and M. Kwiatkowska. Compositional state space reduction using untangled actions. In Proc. 13th International Workshop on Expressiveness in Concurrency (EXPRESS'06), volume 175 of Electronic Notes in Theoretical Computer Science. Technical Report 2006/10, Department of Computing, Imperial College London. August 2006. [pdf] [bib]
Downloads:  pdf pdf (288 KB)  bib bib
Notes: ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Abstract. 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 can be devised for systems with a large number of small processes running in parallel.