Local directed graphs
Dinesh Gambhir · 1992
Model Checkers are tools for the automated verification of concurrent systems. The concurrent system models used by model checkers are typically global state diagrams or petri nets. The size of such reachability system models, and thus search effort and time, explodes exponentially with the size of the concurrent system. This explosion places limits the size of the concurrent systems which can be verified using model checkers. A system model, local directed graphs, which increases the envelope of concurrent systems which may be verified using model checkers is introduced in this dissertation. The local directed graph model is not a monolithic system model like global state diagrams or petri net reachability structures. Instead, the local directed graph model consists of N directed graphs, one for each process composing the concurrent system. Each directed graph describes all possible executions of the process it models with respect to the executions of all other processes. Theoretical and empirical results are presented which show that the local directed graph to be smaller, in most cases, than the corresponding global state diagram model. Algorithms for the generation of local directed graphs, and the construction of a model checkers based on local directed graphs are given. The use of local directed graphs for model checking requires the use of indexing in the temporal logic formula specifying concurrent system properties. The grammar and semantics of a temporal logic language modified for this task, LogicTool CTL, are given. Extensive examples illustrating the use of LogicTool CTL for specifying concurrent system properties are given.