caa a22 4500 605516308 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20151101xx s 000 0 eng 10.1007/s00165-014-0329-4 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0329-4 Untanglings: a novel approach to analyzing concurrent systems [Elektronische Daten] [Artem Polyvyanyy, Marcello La Rosa, Chun Ouyang, Arthur ter Hofstede] Substantial research efforts have been expended to deal with the complexity of concurrent systems that is inherent to their analysis, e.g., works that tackle the well-known state space explosion problem. Approaches differ in the classes of properties that they are able to suitably check and this is largely a result of the way they balance the trade-off between analysis time and space employed to describe a concurrent system. One interesting class of properties is concerned with behavioral characteristics. These properties are conveniently expressed in terms of computations, or runs, in concurrent systems. This article introduces the theory of untanglings that exploits a particular representation of a collection of runs in a concurrent system. It is shown that a representative untangling of a bounded concurrent system can be constructed that captures all and only the behavior of the system. Representative untanglings strike a unique balance between time and space, yet provide a single model for the convenient extraction of various behavioral properties. Performance measurements in terms of construction time and size of representative untanglings with respect to the original specifications of concurrent systems, conducted on a collection of models from practice, confirm the scalability of the approach. Finally, this article demonstrates practical benefits of using representative untanglings when checking various behavioral properties of concurrent systems. British Computer Society, 2015 Concurrency nationallicence Concurrent systems nationallicence Analysis nationallicence Untanglings nationallicence Representative untanglings nationallicence Polyvyanyy Artem Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut La Rosa Marcello Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut Ouyang Chun Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut ter Hofstede Arthur Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 753-788 0934-5043 27:5-6<753 2015 27 165 https://doi.org/10.1007/s00165-014-0329-4 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0329-4 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Polyvyanyy Artem Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut NATIONALLICENCE 700 1- La Rosa Marcello Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut NATIONALLICENCE 700 1- Ouyang Chun Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut NATIONALLICENCE 700 1- ter Hofstede Arthur Queensland University of Technology, P Block (Level 8), Gardens Point Campus, GPO Box 2434, 4001, Brisbane, QLD, Australia aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/5-6(2015-11-01), 753-788 0934-5043 27:5-6<753 2015 27 165