Extended symbolic transition graphs with assignment

Author

Deng, Weijia ; Lin, Huimin

Author_Institution

Inst. of Software, Chinese Acad. of Sci., Beijing, China

Volume

1

fYear

2005

fDate

26-28 July 2005

Firstpage

227

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 2005. COMPSAC 2005. 29th Annual International

ISSN

0730-3157

Print_ISBN

0-7695-2413-3

Type

conf

DOI

10.1109/COMPSAC.2005.76

Filename

1510024