Sciweavers

Share
ENTCS
2006

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

8 years 8 months ago
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...
Tobe Toben, Bernd Westphal
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Tobe Toben, Bernd Westphal
Comments (0)
books