Jonathan Certes

Home / Resources / Definition of PSL operators as syntactic sugar for LTL

Introduction

Coq is an interactive theorem prover. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

LTL_Coq is a library developed by Cenobio Moisés Vázquez Reyes and available here . It contains a simple formalization of many LTL concepts and theorems. This includes definitions of formulas, paths and LTL semantics. LTL (Linear Temporal Logic) is a modal temporal logic with modalities referring to time.

NuSMV is an open-source model checker which implements symbolic model-checking, using a fixed point algorithm with Binary Decision Diagrams (BDD), where a set of states is represented by a BDD instead of an exhaustive list of individual states. Models are described in SMV language and NuSMV supports the analysis of specifications expressed as invariants or in temporal logics, including LTL and PSL.

pyNuSMV is a Python binding for NuSMV. It is intended to provide a Python interface to NuSMV, allowing to use NuSMV as a library.

Coq source code

PSL operators are mostly syntactic sugar for LTL, which means that we need a definition of LTL semantics first. We rely on the LTL_Coq library. Alos, it means that we can define these operators in Coq with a recursive definition. This is achieved with the Fixpoint keyword.

Require Import Nat.
Require Import LTL.

Infix "-->" := impP (at level 20).

Fixpoint next_event_a_i (b: PathF) (i: nat) (f: PathF) :=
  match i with
  | 0   => bot
  | 1   => ((negP b) U (b ∧ f)) ∨ G(negP b)
  | S n => ((negP b) U (b ∧ (X (next_event_a_i b n f)))) ∨ G(negP b)
  end.

Fixpoint next_event_a (b: PathF) (i j: nat) (f: PathF) :=
  match j with
  | 0   => (next_event_a_i b i f)
  | S n =>
    if ( j <? i ) then
      bot
    else
      if ( j =? i ) then
        (next_event_a_i b i f)
      else
        (next_event_a b i n f) ∧ (next_event_a_i b (n+1) f)
  end.

Definition next_event (b f : PathF) := (next_event_a b 1 1 f).

To observe the behaviour of these operators, we can compute some examples.

Section examples.
  Variable (a b: At).
  Compute (next_event   (Var a)     (Var b)).
  Compute (next_event_a (Var a) 1 1 (Var b)).
  Compute (next_event_a (Var a) 2 2 (Var b)).
  Compute (next_event_a (Var a) 3 3 (Var b)).

  Compute (next_event_a (Var a) 1 2 (Var b)).
  Compute (next_event_a (Var a) 2 3 (Var b)).
  Compute (next_event_a (Var a) 1 3 (Var b)).
End examples.

Verification with NuSMV

Model checker NuSMV provides a function to convert PSL to LTL. We can rely on pyNuSMV to convert the same examples and verify that we obtain the same semantic.

First, we need to write the same examples with SMV syntax, for instance in a file called spec.smv:

MODULE main

PSLSPEC next_event("a")("b");

PSLSPEC next_event_a("a")[1:1]("b");
PSLSPEC next_event_a("a")[2:2]("b");
PSLSPEC next_event_a("a")[3:3]("b");

PSLSPEC next_event_a("a")[1:2]("b");
PSLSPEC next_event_a("a")[2:3]("b");
PSLSPEC next_event_a("a")[1:3]("b");

Then, we write a Python script and import pynusmv. Let's imagine that we have a function recursivelyGetAllNodes() that returns all nodes with the same type from the AST.

import pynusmv
import pynusmv.nusmv.parser.psl.psl

pynusmv.init.init_nusmv()
pynusmv.nusmv.parser.parser.Parser_ReadSMVFromFile("spec.smv")

theTree = pynusmv.nusmv.parser.parser.cvar.parsed_tree
theList = list()
recursivelyGetAllNodes(theTree, pynusmv.nusmv.parser.parser.PSLSPEC, theList)
theList.reverse()

for theSpecNode in theList:
  # separate the name from the property:
  theNameNode = pynusmv.nusmv.node.node.cdr(theSpecNode)
  thePslNode  = pynusmv.nusmv.node.node.car(theSpecNode)
  # convert PSL property to LTL:
  theLtlNode = pynusmv.nusmv.parser.psl.psl.PslNode_convert_psl_to_core(thePslNode)
  #
  thePslString = pynusmv.nusmv.node.node.sprint_node(thePslNode)
  theLtlString = pynusmv.nusmv.node.node.sprint_node(theLtlNode)
  print(thePslString)
  print(" <-> " + theLtlString)
  print("")

Makefile

Compilation of a Coq program is conducted by coqc. We must compile both the library and our program to observe the computation examples.

Also, we must run our Python script to compare the results.

Here is a Makefile that provides the recipe (make sure to indent with tabulations):

PROOF = proof.v
DEPS  = LTL.v

BASENAME = $(basename ${PROOF})
DEPSNAME = $(basename ${DEPS})

all: ${PROOF} $(addsuffix .vos, ${DEPSNAME}) verify.py spec.smv
    coqc -verbose ${PROOF}
    @echo "The proof has run correctly."
    ./verify.py

%.vos : %.v
    coqc -verbose $^

clean:
    $(RM) $(addsuffix .glob, ${DEPSNAME}) $(addsuffix .vo  , ${DEPSNAME})
    $(RM) $(addsuffix .vok , ${DEPSNAME}) $(addsuffix .vos , ${DEPSNAME})
    $(RM) $(addsuffix .aux , $(addprefix ., ${DEPSNAME}))
    $(RM) $(addsuffix .glob, ${BASENAME}) $(addsuffix .vo  , ${BASENAME})
    $(RM) $(addsuffix .vok , ${BASENAME}) $(addsuffix .vos , ${BASENAME})
    $(RM) $(addsuffix .aux , $(addprefix ., ${BASENAME}))

Associated resources

Here is an archive which contains the discussed example and its Makefile. Library LTL_Coq is not distributed here, please refer to its repository to download it.

---