Language Inclusion for Finite Prime Event Structures

TL;DR

This paper investigates language inclusion problems for finite prime event structures, offering complexity results, a decision algorithm, and practical evaluation, highlighting the advantages of prime event structures in representing concurrent systems.

Contribution

It introduces a decision algorithm for language inclusion in prime event structures, leveraging their succinctness and demonstrating practical applications in test case generation.

Findings

Prime event structures can be exponentially more succinct than other formalisms.

The paper provides a complexity analysis for inclusion and membership problems.

An implemented algorithm shows effectiveness on benchmark examples.

Abstract

We study the problem of language inclusion between finite, labeled prime event structures. Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems. A labeled prime event structure induces a language of sequences of labels produced by the represented system. We study the problem of deciding inclusion and membership for languages encoded by finite prime event structures and provide complexity results for both problems. We provide a family of examples where prime event structures are exponentially more succinct than formalisms that do not take concurrency into account. We provide a decision algorithm for language inclusion that exploits this succinctness. Furthermore, we provide an implementation of the algorithm and an evaluation on a series of benchmarks. Finally, we demonstrate how our results can be applied to mutation-based test case generation.