Symbolic Counter-Examples Generation For Discrete Real-Time Temporal Epistemic Logic

One of the most important features of model checking is the ability to generate a counterexample for a temporal property verified false.The counterexample provides engineers with debugging information to explain the violation of the verified prop erty.However,in the development of model checking,up to now little research effort has been put into counterexamples.The existing symbolic model checkers are not sufficiently expressive in specification descriptions.They can only verify a small subset of real-time temporal logic with epistemic.For counterexample generation,most them are relatively simple,incomplete and lack of suitable annotations for intelligibility.Therefore,a new real-time branching temporal epistemic logic RTCTL~*K,is proposed for the first time.It is an extension of the c omputation tree logic CTL~* with discrete time bounds and epistemic logic,which makes it easy for us to describe and verify the real-time properties,the epistemic states of agents and the epistemic reachability of for agents in a certain time interval.Then we present the symbolic counterexample generation algorithms based on testers,and deeply extend and implement the new model checker,so that it can automatically generate very concise graphical counterexample s for RTCTL~*K,which is easier to analyze intuitively.The main work of this paper is to define the syntax and semantics of RTCTL~*K,to propose a counterexample generation algorithm and to implement a symbolic model checker—MCTK2,as follows:(1)We first define the more expressive real-time branching temporal epistemic logic,RTCTL~*K,which is an extension of CTL~* with discrete time bounds and epistemic logic.(2)Based on just discrete systems(JDS),we propose algorithms of counterexample generation for RTCTL~*K.The generated counterexamples are state transition directed graphs of branching structure,in which states and transitions may be attached with a list of true sub-formulas as annotations for good intelligibility,all strongly connected components are cycles and the corresponding component gr aph is tree-like.Furthermore,in order to avoid creating large tree-like model graphs,the witness of subformulas will be generated according to the users' requirements.Because each node on the graph is interactive,for each unexplained sub-formula(preceded by path quantifier s or epistemic operators)attached on a state,when the user clicks the state,a new branch is created from the current state.we proved our algorithms of counterexample generation are complete for the universal fragment of RTCTL~*K with respect to JDS.(3)We develop a symbolic model checker MCTK2 for RTCTL~*K,in which the proposed counterexample generating algorithm is implemented.through a series of experiments compared with the famous model checkers,nuXmv and MCTK2,the experimental results demonstrate that compared with nuXmv,MCTK2 is superior to it in verifying RTLTL formulas and generating counter-examples,in ease of use,time consumption and memory usage for verifying CTL~*K,RTLTL and RTCTL~* formulas and generating counter-examples,MCTK2 is superior to MCMAS.