Title :
Extended symbolic transition graphs with assignment
Author :
Deng, Weijia ; Lin, Huimin
Author_Institution :
Inst. of Software, Chinese Acad. of Sci., Beijing, China
Abstract :
An extension of symbolic transition graphs with assignment is proposed which combines the advantages of both the assignment-before-action and the assignment-after-action approaches: like the former it allows a simple set of rules to be designed for generating finite symbolic graphs from regular value-passing process descriptions; like the later it avoids creating multiple copies in the graph for a recursive process definition. Experiences show that, in most cases, considerable reductions in verification time and space can be achieved using the new approach.
Keywords :
bisimulation equivalence; concurrency control; formal verification; graph theory; process algebra; recursive functions; scheduling; assignment; assignment-after-action; assignment-before-action; bisimulation checking; concurrent systems; extended symbolic transition graphs; finite symbolic graphs; formal verification; model checking; process algebra; recursive process definition; value-passing process description; Algebra; Application software; Carbon capture and storage; Computer applications; Computer science; Laboratories; Concurrent systems; bisimulation checking; model checking; process algebra; symbolic transition graphs; value-passing; verification;
Conference_Titel :
Computer Software and Applications Conference, 2005. COMPSAC 2005. 29th Annual International
Print_ISBN :
0-7695-2413-3
DOI :
10.1109/COMPSAC.2005.76
