An Automaton Model to Succinctly Represent Suffix-Based Specifications of a Concurrent System
摘要
Deterministic Suffix-reading Automata (DSA) were introduced recently as a concise model for regular languages. DSAs can succinctly capture formal specifications that are based on sequences of input actions (and not just single actions). For a concurrent system, specifications may further depend on combinations of input sequences seen across multiple components (ports). For such systems, DSAs consider all possible interleavings, resulting in large and unreadable automata. In this work, we enrich DSAs to include a \(\parallel \) operator in its transitions. The resulting multi-port DSAs (mDSAs) can succinctly represent concurrent suffix-based specifications. Subsequently, we extend mDSAs to produce outputs on transitions, and show that state reachability becomes PSPACE-complete in the presence of outputs. Finally, we apply our results to the formal analysis of Expressive Decision Tables (EDT) – an industry notation for specifying requirements of reactive systems.