DocumentCode
1942806
Title
Symbolic Model Checking APSL
Author
Liu, Wanwei ; Wang, Ji ; Chen, Huowang ; Ma, Xiaodong
Author_Institution
Sch. of Comput., Nat. Univ. of Defense Technol., Harbin
fYear
2008
fDate
17-19 June 2008
Firstpage
39
Lastpage
46
Abstract
PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper, we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover, we show how to implement this algorithm via the BDD based symbolic approach.
Keywords
finite automata; temporal logic; finite automata; symbolic model checking; temporal logic; Automata; Binary decision diagrams; Boolean functions; Concurrent computing; Data structures; Distributed computing; Distributed processing; Laboratories; Logic; Software engineering; PSL; Symbolic model checking;
fLanguage
English
Publisher
ieee
Conference_Titel
Theoretical Aspects of Software Engineering, 2008. TASE '08. 2nd IFIP/IEEE International Symposium on
Conference_Location
Nanjing
Print_ISBN
978-0-7695-3249-3
Type
conf
DOI
10.1109/TASE.2008.24
Filename
4549884
Link To Document