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
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;
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
DOI :
10.1109/TASE.2008.24
