Premium
Efficient encoding for bounded model checking of timed automata
Author(s) -
Chen Zuxi,
Xu Zhongwei,
Du Junwei,
Mei Meng,
Guo Jing
Publication year - 2017
Publication title -
ieej transactions on electrical and electronic engineering
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.254
H-Index - 30
eISSN - 1931-4981
pISSN - 1931-4973
DOI - 10.1002/tee.22457
Subject(s) - computer science , satisfiability , bounded function , encoding (memory) , satisfiability modulo theories , scalability , automaton , encode , boolean satisfiability problem , modulo , reduction (mathematics) , theoretical computer science , computability , model checking , solver , state space , semantics (computer science) , algorithm , mathematics , discrete mathematics , programming language , artificial intelligence , mathematical analysis , biochemistry , chemistry , statistics , geometry , database , gene
Bounded model checking (BMC) of timed automata has been successfully applied to verify concurrent real‐time systems, but its scalability is still limited by the large bound required to find counter‐example, the efficiency of the decision procedure which is employed to solve the BMC formula, as well as the large search space for solving satisfiability of the resulting formula. In this paper, we present a systemic encoding scheme to attack all the above three problems. To attack the first problem, we first encode a discrete action followed by a time delay as a composed transition to cut the BMC steps which are used to characterize the time elapse. Then we take advantage of the local time semantics to allow more independent actions to be executed in parallel, which further reduces the required number of BMC steps and hence also the formula size. To employ a more efficient decision procedure, we also translate the linear arithmetic encoding of timed automata to a difference logic formula which can be solved more efficient by a satisfiability modulo theory solver. To address the last problem, we employ explicit‐state partial order reduction idea of only executing some of the enabled transitions to add additional constrains to eliminate some redundant multi‐step executions, thus restricting the search space. Experimental results show that our encoding performs significantly better than previous encodings. © 2017 Institute of Electrical Engineers of Japan. Published by John Wiley & Sons, Inc.