Compact and efficiently verifiable models for concurrent systems.

*(English)*Zbl 1425.68301Summary: Partial orders are a fundamental mathematical structure capable of representing concurrency and causality on a set of atomic events. In many applications it is essential to consider multiple partial orders, each representing a particular behavioral scenario or an operating mode of a system. With the exploding growth of the complexity of systems that software and hardware engineers design today, it is no longer feasible to represent each partial order of a large system explicitly, therefore compressed representations of sets of partial orders become essential for improving the scalability of design automation tools. In this paper we study two well known mathematical formalisms capable of the compressed representation of sets of partial orders: Labeled Event Structures and Conditional Partial Order Graphs. We discuss their advantages and disadvantages and propose efficient algorithms for transforming a set of partial orders from a given compressed representation in one formalism into an
equivalent representation in another formalism without explicitly enumerating every partial order. The proposed algorithms make use of an intermediate mathematical formalism which we call Conditional Labeled Event Structures that combines the advantages of both structures. Finally, we compare these structures on a number of benchmarks coming from concurrent software and hardware domains.

##### MSC:

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

06A06 | Partial orders, general |

68P30 | Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science) |

PDF
BibTeX
XML
Cite

\textit{H. Ponce de León} and \textit{A. Mokhov}, Form. Methods Syst. Des. 53, No. 3, 407--431 (2018; Zbl 1425.68301)

Full Text:
DOI

##### References:

[1] | ARM Ltd.: ARMv6-M Architecture Reference Manual (2010) |

[2] | Berkeley Logic Synthesis and Verification Group: ABC: a System for Sequential Synthesis and Verification, Release 70930. http://www.eecs.berkeley.edu/ alanmi/abc/ |

[3] | Brookes, S.; O’Hearn, PW, Concurrent separation logic, ACM SIGLOG News, 3, 47-65, (2016) |

[4] | D’Alessandro C, Mokhov A, Bystrov AV, Yakovlev A (2007) Delay/phase regeneration circuits. In: 13th IEEE international symposium on asynchronous circuits and systems (ASYNC 2007), 12-14 March 2006, Berkeley, California, USA. IEEE Computer Society, pp 105-116. https://doi.org/10.1109/ASYNC.2007.14 |

[5] | Diekert V, Rozenberg G (eds) (1995) The book of traces. World Scientific Publishing Co., Inc, Singapore |

[6] | Esparza, J.; Rozenberg, G. (ed.); Reisig, W. (ed.), Decidability and complexity of petri net problem-an introduction, 374-428, (1998), Berlin · Zbl 0926.68087 |

[7] | Esparza J, Heljanko K (2008) Unfoldings—a partial-order approach to model checking. In: Monographs in theoretical computer science. An EATCS series. Springer · Zbl 1153.68035 |

[8] | Godefroid P, Van Leeuwen J, Hartmanis J, Goos G, Wolper P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, vol 1032. Springer, Heidelberg |

[9] | Haar S, Rodríguez C, Schwoon S (2013) Reveal your faults: it’s only fair! In: ACSD, pp 120-129 |

[10] | Kähkönen K, Heljanko K (2014) Testing multithreaded programs with contextual unfoldings and dynamic symbolic execution. In: 14th international conference on application of concurrency to system design, pp 142-151. https://doi.org/10.1109/ACSD.2014.20 |

[11] | Khomenko V, Mokhov A (2011) An algorithm for direct construction of complete merged processes. In: International conference on application and theory of Petri Nets and concurrency. Springer, pp 89-108 · Zbl 1330.68206 |

[12] | McMillan, K.; Probst, DK (ed.); Bochmann, G. (ed.), Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, 164-177, (1993), Heidelberg |

[13] | Milner R (1980) A calculus of communicating systems, vol 92. Springer, Berlin · Zbl 0452.68027 |

[14] | Mokhov A (2009) Conditional partial order graphs. Ph.D. thesis, Newcastle University |

[15] | Mokhov, A.; Khomenko, V., Algebra of parameterised graphs, ACM Trans Embed Comput Syst, 13, 143, (2014) |

[16] | Mokhov, A.; Yakovlev, A., Conditional partial order graphs: model, synthesis, and application, IEEE Trans Comput, 59, 1480-1493, (2010) · Zbl 1368.68273 |

[17] | Mokhov, A.; Alekseyev, A.; Yakovlev, A., Encoding of processor instruction sets with explicit concurrency control, IET Comput Digital Tech, 5, 427-439, (2011) |

[18] | Mokhov, A.; Iliasov, A.; Sokolov, D.; Rykunov, M.; Yakovlev, A.; Romanovsky, A., Synthesis of processor instruction sets from high-level ISA specifications, IEEE Trans Comput, 63, 1552-1566, (2014) · Zbl 1364.68038 |

[19] | Nielsen, M.; Plotkin, GD; Winskel, G., Petri nets, event structures and domains, part I, Theoret Comput Sci, 13, 85-108, (1981) · Zbl 0452.68067 |

[20] | Poliakov, I.; Sokolov, D.; Mokhov, A.; Kleijn, J. (ed.); Yakovlev, A. (ed.), Workcraft: a static data flow structure editing, visualisation and analysis tool, 505-514, (2007), Berlin |

[21] | Ponce de León H, Mokhov A (2015) Building bridges between sets of partial orders. In: 9th international conference on language and automata theory and applications, LATA 2015, Nice, France, March 2-6, 2015, Proceedings, pp 145-160 · Zbl 1451.68193 |

[22] | Ponce de León H, Rodríguez C, Carmona J, Heljanko K, Haar S (2015) Unfolding-based process discovery. In: 13th international symposium on automated technology for verification and analysis, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, Lecture Notes in Computer Science, vol 9364. Springer, pp 31-47 |

[23] | Quinlan, JR, Induction of decision trees, Mach Learn, 1, 81-106, (1986) |

[24] | Rodríguez C, Sousa M, Sharma S, Kroening D (2015) Unfolding-based partial order reduction. In: 26th international conference on concurrency theory, CONCUR 2015, Madrid, Spain, September 1-4, 2015, pp 456-469 · Zbl 1374.68342 |

[25] | Rykunov M (2013) Design of asynchronous microprocessor for power proportionality. Ph.D. thesis, Newcastle University |

[26] | Saarikivi, O.; Ponce de León, H.; Kähkönen, K.; Heljanko, K.; Esparza, J., Minimizing test suites with unfoldings of multithreaded programs, ACM Trans Embed Comput Syst, 16, 45:1-45:24, (2017) |

[27] | Valmari A (1998) The state explosion problem. In: Lectures on Petri nets I: basic models. Springer, pp 429-528 |

[28] | van Beest NRTP, Dumas M, García-Bañuelos L, Rosa ML (2015) Log delta analysis: interpretable differencing of business process event logs. In: 13th international conference on business process management, BPM 2015, Innsbruck, Austria, August 31-September 3, 2015, Proceedings, pp 386-405 |

[29] | Wegener I (1987) The complexity of boolean functions. Johann Wolfgang Goethe-Universitat, Frankfurt · Zbl 0623.94018 |

[30] | Workcraft webpage (2017) www.workcraft.org |

[31] | Zhang, L.; Malik, S.; Brinksma, D. (ed.); Larsen, KG (ed.), The quest for efficient boolean satisfiability solvers, 17-36, (2002), Berlin · Zbl 1010.68530 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.