Package eu.iv4xr.framework.extensions.ltl

Class BuchiModelChecker

java.lang.Object
eu.iv4xr.framework.extensions.ltl.BuchiModelChecker
public class BuchiModelChecker extends Object
Provide an explicit-state bounded and lazy model checker that can be used to check if a model M has an execution, of up to some maximum length, that would satisfy a certain property. The property is encoded as a Buchi automaton B. We implement the double DFS model checking algorithm, similar to the one used by the SPIN model checker.

An infinite execution of M satisfies this property if it is accepted by the Buchi automated B. B does not literally check infinite executions, as this would be impossible. Instead, B is used to look for a witness that it can accept. A witness is a finite execution, but it implicitly extensible to a set of infinite exectutions, all of them would be accepted by B. The model-checker only needs to find such a witness.

For practicality, the model-checking is made 'bounded'. This means that it only searches for witness of some given maximum length. This allows us to handle an M that has infinite state space.

When a witness is found (so M can produce an infinite execution that satisfies B), the witness will be returned. Note that failing to find such a witness means that the negation of the property induced by B therefore holds globally on all executions of M within the maximum depth from the model's initial state.

The model checker can be used to target any 'program' or 'model of program' that implements the interface ITargetModel.

Author:
Wish

  • Field Details

    • model

      public ITargetModel model
      The 'program' or 'model of a program' that we want to target in model-checking.

    • stats

      public BasicModelChecker.MCStatistics stats
      Hold some basic statistics over the last model-checking run.

  • Constructor Details

    • BuchiModelChecker

      public BuchiModelChecker​(ITargetModel model)

  • Method Details

    • sat

      public SATVerdict sat​(LTL<IExplorableState> phi)
      Check if the target 'program' model can produce an infinite execution that would satisfy the given LTL formula.

    • sat

      public SATVerdict sat​(Buchi buchi)
      Check if the target 'program' model can produce an infinite execution that would be accepted by the given Buchi automaton. If so SAT is returned, and else UNSAT. Be careful that this method may not terminate if the target program has an infinite state space. Use sat(Buchi, int) instead.

    • sat

      public SATVerdict sat​(LTL<IExplorableState> phi, int maxDepth)
      Check if the target program has an finite execution of the specified maximum length that would witness the given LTL formula.

    • sat

      public SATVerdict sat​(Buchi buchi, int maxDepth)
      Check if the target program has an finite execution of the specified maximum length, that ends in a state satisfying the predicate q. If so, it returns SAT, and else UNSAT.

    • find

      public BasicModelChecker.Path<Pair<IExplorableState,​String>> find​(LTL<IExplorableState> phi, int maxDepth)
      The same as find(Buchi, int), but it takes an LTL formula for specifying the pattern of the execution to find. This returns witness for the given LTL property.

    • findShortest

      public BasicModelChecker.Path<Pair<IExplorableState,​String>> findShortest​(Buchi buchi, int maxDepth)
      Similar to find(Buchi, int), but it will return the shortest execution (of the specified max-length) that satisfies the Buchi.

    • findShortest

      public BasicModelChecker.Path<Pair<IExplorableState,​String>> findShortest​(LTL<IExplorableState> phi, int maxDepth)
      Similar to find(LTL, int), but it will return the shortest execution (of the specified max-length) that satisfies the given LTL.

    • find

      public BasicModelChecker.Path<Pair<IExplorableState,​String>> find​(Buchi buchi, int maxDepth)
      Check if the target 'program' model can produce an infinite execution that would be accepted by the given Buchi automaton. If so a witness is returned, and else null.

      A 'witness' is a finite execution, that can be 'extended' to a infinite execution accepted by the Buchi. Further explanation about this can be found here: Buchi.

    • dfsBuchi

      BasicModelChecker.Path<Pair<IExplorableState,​Integer>> dfsBuchi​(Buchi buchi, BasicModelChecker.Path<Pair<IExplorableState,​Integer>> pathSoFar, Set<Pair<IExplorableState,​Integer>> statesInPathToStartOfPossibleCycle, Set<Pair<IExplorableState,​Integer>> visitedStates, Pair<IExplorableState,​Integer> state, int remainingDepth)
      The worker of our LTL model-checking algorithm. It is a depth-first search (DSF) algorithm. The same algorithm as used in the SPIN model checker. It actually perforsm a double-DFS search. To search a witness (an execution of the 'program' that would be accepted by the given Buchi), the algorithm uses DSF to find either a reachable state that would be non-omega-accepted by the Buchi, or to find a reachable cycle that is omega-accepted by the Buchi. In the second case, DFS is used to find an O-accepting state o, and then a second DSF is used if to check if there is a path that starts from o and cycle back to o (which means that we would then have omega acceptance).
      Parameters:
      buchi - The Buchi automaton that defines the property to check.
      pathSoFar - The execution that leads to current state to explore (the state parameter below; so it is the path up to and including that state).
      statesInPathToStartOfPossibleCycle - The set of states to the start of a possible cycle over omega-accepting states. The start of such cycle is always an omega-accepting state. We keep track of this information to make cycle detection more efficient.
      visitedStates - The set of states that have been visited by the DFS.
      state - The current state to explore next.
      remainingDepth - The remaining depth. When this becomes 0, the DFS will not explore the given state (the recursion will just return with null).
      Returns:
      An execution path (whose length is at most the specified depth), satisfying the property described by Buchi, if there is one.