Tableaux-based decision procedures for fixed point logics
Creators: name: Widmann, Florian
Publisher: name: The Australian National University
Year: 2010
Subjects: Modality (Logic)
Logic, Symbolic and mathematical
Computer programs
Correctness

description: Modal fixed point logics are a useful formalism to specify and verify correctness of reactive systems such as computer operating systems, network communication protocols, or air traffic control systems. One characteristic of reactive systems is that they are non-terminating and maintain an ongoing interaction with the environment. Modal fixed point logics allow us to specify properties like "a deadlock will never happen" which are particularly useful for such systems. One of the important questions associated with fixed point logics is the satisfiability problem: given a formula representing a specification, does there exist a situation in which the formula holds. An algorithm for deciding satisfiability can be used, for example, to automatically check whether a specification is inconsistent. Since an inconsistent specification cannot be satisfied in any structure, it most likely indicates an error in the specification. For many modal fixed point logics there exist algorithms, also called decision procedures, which decide whether or not a given formula is satisfiable. To be useful in practice, however, it is also crucial that these algorithms return their results in "reasonable" time. It is no use if an algorithm takes a hundred years to determine whether a formula is satisfiable. One difficulty in deciding satisfiability is related to formulae which capture properties like "eventually something will happen". Such formulae are called eventualities and we say that they have to be fulfilled. Intuitively, at any given moment, it is difficult to establish that an eventuality will never be fulfilled since we have to rule out the possibility that it will be fulfilled at some future time. Traditional tableau-based decision procedures for modal fixed point logics proceed in multiple passes. In the first pass, they build a graph corresponding to a putative structure for the input formulae. In the subsequent passes, they then check if all eventualities can be fulfilled in the graph. If an eventuality cannot be fulfilled, the corresponding node is pruned, which might lead to other nodes being pruned in later passes. Since the whole graph is built first, before eventualities are considered, it is quite possible that much of the work is needless and might have been avoided if we could detect unfulfilled eventualities earlier. This thesis investigates techniques to efficiently handle eventualities. We present decision procedures for several fixed point logics which use an "on-the-fly" approach to find unfulfilled eventualities as early as possible and potentially save unnecessary work. Our algorithms are based on tableaux which have proven to be successful for deciding satisfiability for related logics. All algorithms are described in detail and are accompanied by formal correctness proofs. Furthermore, the algorithms have been implemented and can be downloaded (see below). We also compare our provers with existing provers using formula-classes from the literature when possible. For some logics, our implementations are the first theorem provers for these logics. More specifically, the problems and techniques are as follows. Our first approach builds a cyclic but finite tree where the status of each node is determined only once depending on the status of its children. That is, the algorithm needs only one pass. In order to handle eventualities, we need additional data structures which track the fulfilment status of the eventualities. We give two variants. One variant can decide at the bottom of the tree whether the corresponding cycle is "bad". The other variant cannot decide at the bottom but passes information up the tree and detects "bad" cycles when it reaches the root of a "closed" subtree. Since both procedures build a tree, they are not complexity-optimal. Our second approach basically interleaves the multiple passes of traditional tableaux to obtain a complexity-optimal graph-based procedure. To handle eventualities "on-the-fly", we track the fulfilment status of each eventuality using the graph nodes which are older than the node which contains the eventuality. If an eventuality can reach a node which is younger than its corresponding node, the younger node is a called a potential rescuer because the eventuality might be fulfilled via this potential rescuer in some future part of the graph. Once an eventuality cannot be fulfilled in the older part of the graph and does not have any potential rescuers, it cannot be fulfilled in the graph, now or in the future, and the corresponding node can be pruned. We also present a complexity-optimal technique to handle inverse roles and symmetric relations which does not require a cut rule. The method uses a new type of node called a special node. These special nodes "restart" states which turned out to be "too small" and link their "bigger" versions into the graph. We then combine potential rescuers and special nodes to give the first complexity-optimal and cut-free tableau procedure for CPDL.