Concurrent LSC Verification: On Decomposition Properties of Partially Ordered Symbolic Automata

Partially Ordered Symbolic Automata (POSAs) are used as the semantical foundation of visual formalisms like the scenario based language of Live Sequence Charts (LSCs). To check whether a model satisfies an LSC requirement, the LSC's POSA can be composed in parallel to the model as an observer automaton or it can be translated to a CTL or LTL formula. Thus by the well-known complexity properties of CTL and LTL model-checking, the size of an LSC's POSA directly contributes to the runtime of the model-checking task. This size grows with the concurrency allowed by the LSC, e.g. when the observation order of LSC elements is relaxed by enclosing them in a coregion. We investigate decomposition properties of POSAs with deterministic states, i.e. states with disjointly annotated outgoing transitions. We devise a procedure to decompose a POSA with deterministic states into a set of POSAs whose intersection language is equal to the language of the original POSA. When decomposing at dom...

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Tobe Toben, Bernd Westphal
• Keywords: ENTCS 2006, Live Sequence Charts, LSC Requirement, Scenario Based Language