UniTO/tesi/galla/tesi.org

An automata-based implementation of a symbolic CTL* model checker

\begin{abstract} This dissertation presents the implementation of a symbolic CTL* model checking algorithm based on multi-valued decision diagrams (MDDs). Given a Petri Net model and a CTL* proposition, the algorithm is capable of identifying LTL sub-formulae, translate them to Büchi automata and compute the synchronized product of each LTL formula with the model. MDDs are used to encode the Petri Net and such composition, provably lowering both system memory and time required to manipulate its graph of reachable states with respect to explicit model checking tecniques. By combining the sets of satisfying states for each LTL sub-formula according to the temporal quantifiers preceding them, the algorithm is capable of producing the boolean satisfaction result of the CTL* formula and a counterexample or witness run describing such outcome. Timed test runs executed againts a large set of models and specifications of LTL, CTL and CTL* temporal logics show competitive performance results with respect to other tools which process CTL* by translating each formula to $\mu$-calculus. This algorithm has been implemented as one of the free and open source programs composing the GreatSPN framework for formal verification of systems. \end{abstract}

Introduction

Model Checking

Model checking is a formal verification technique intended to analyze properties of system designs. Given a formal model and a specification, the objective of model checking is to decide whether the behavior of the model satisfies the specification or not. The model is usually represented as a Kripke structure or by a high-level formalism that can be transformed into a Kripke structure. Examples of these formalisms are Petri Nets and Process algebra.

The specification is provided using a temporal logic expression, that is, a formula that expresses a temporal and logical statement. Temporal logics are modal logics geared towards the description of the temporal ordering of events. It is important to clarify that these logics do not consider precise timing requirements of activities or events, but reason about their abstract temporal order. For this reason, they are particularly useful when applied to concurrent systems in which all components proceed in a lock-step fashion over a discrete time domain. The system behavior is assumed to be observable at integral time points and each time point identifies a snapshot of all variables of the system, called state.

Two brands of temporal logics have been proposed over the years for specifying the properties of reactive systems. Linear Temporal Logic \cite{Pnueli77} is based on linear time, therefore considering every moment in time as having a unique possible future. Computational Tree Logic \cite{ClarkeE81} is defined upon branching time: it pictures the structure of time as a tree, allowing each moment in time to split into different possible futures. From now on we will refer to these two logics using their well-known acronyms LTL and CTL respectively.

The difference between LTL and CTL is rooted in their satisfaction relations, which are conceptually different. LTL is said to be path-based, since a system S satisfies a LTL formula ɸ if for all initial paths of S, paths starting in an intial state $s_{\textit{0}}$ satisfy ɸ. Conversely, CTL is said to be state-based, since a system S satisfies a CTL formula ɸ if and only if ɸ holds in all initial states of S.

Furthermore, the expressiveness of LTL and CTL temporal logics is incomparable \cite{Lamport80}. Conversely, CTL is particularly useful to express the possibility of existence of a specific path of execution of a model, that is, the occurrence of an event happening on one branch but not necessarily all of them. This concept cannot be expressed using a formalism based on linear time such as LTL, which describes executions of a system, not the way those executions are organized in a branching tree. On the contrary, CTL cannot express situations in which the same behavior may occur on distinct branches at distinct times, while the ability of LTL to describe individual paths is more convenient in this case. In practice, the LTL formula FGɸ is not expressible in CTL, while the formula AFAGɸ is not expressible in LTL. Given the shortcomings of both these temporal logics, a superset of LTL and CTL called CTL* \cite{EmersonH86} has been introduced. \\

A brief history of LTL model checking

Model checking LTL properties comes down to checking language emptyness of the syncronized product between the Kripke structure representing the model and a formalism which can represent a LTL formula while being translatable to a Kripke structure, namely a Büchi automaton. This automata-theoretic approach \cite{Vardi95} treats the synchronized product as a transition system \cite{Keller76} whose state graph can be analyzed using tecniques classified in two main categories:

• Explicit methods process the state graph of the synchronized product using graph traversal algorithms.
• Symbolic methods represent the state graph using decision diagrams and usually apply fixed point algorithms to the set of states to find the strongly connected components (SCCs) of the transition system.

Explicit methods are based on graph traversal algorithms but are often limited by the complexity of the LTL model checking problem, which is constrained by the size of the state space of the model, the size of the underlying automaton used to represent the formula and the combined size of the two Kripke structures in a transition system. More specifically, the model checking problem for LTL is known to be PSPACE-complete \cite{Sistlac85}. Historically, the first LTL model checkers were explicit: a notable example is SPIN \cite{Holzmann97}, which takes advantage of an optimized version of Tarjan DFS algorithm for finding strongly connected components in a graph, called Nested Depth First Search \cite{HolzmannPy96}.

In practice, model checkers applied to complex, real-world sistems have to face the state space explosion problem: the exponential growth in the number of variables of the state graph dimension. Given that, in general, a system with n variables over a domain of k possible values requires at least $n^{\textit{k}}$ states in the reachability set, it is understandable how even a simple model might necessitate a large reachability graph. Furthermore, dealing with real-valued variables, which have infinite possible assignments, results in a reachability graph with infinitely many states.

This problem has encouraged the development of various tecniques which have proven to be successful in mitigating the state explosion. Explicit model checkers have introduced on-the-fly state-space construction to avoid storing the whole state graph. The most basic on-the-fly algorithm \cite{FernandezMJJ92} stores states which have already been visited in memory and is therefore able to check for cycles in the reachability graph while generating it through DFS. SPIN uses on-the-fly state graph construction combined with partial order reduction \cite{Peled96}, a tecnique which reduces the size of the reachability graph by exploiting commutativity of concurrently executed transitions which result in the same state.

The origin of symbolic model checking

Efforts towards state space minimization have been particularly successful in developing clever representation of the state graph. Symbolic model checking represent the system model and the LTL formula using set of states and set of transitions. These sets can be represented as solutions to logical equations, using decision diagrams to represent this state space implicitly. Since syntactically small equations can represent large set of states, this tecnique ultimately avoids building the state graph explicitly, thus saving space in memory. Above all, Ordered Binary Decision Diagrams (OBDDs) provide a canonical form for boolean formulae which can be substantially more compact than conjunctive or disjuntive normal form and efficient algorithms have been implemented for manipulating them. McMillan was the first to introduce the use of OBDDs to represent the state space of a model, developing a CTL model checking tool called SMV \cite{SymbMC}. Symbolic model checking is considered to be one of the biggest breakthrough in the history of model checking for its impact on the state explosion problem \cite{Clarke08}.

Symbolic model checking was initially applied to CTL because of the significantly lower complexity of the model checking problem with respect to LTL: CTL model checking is known to be P-Complete and its time complexity is bilinear in the size of the model and of the formula \cite{ClarkeES86}. After the introduction of SMV, further research work increased the capabilities of decision diagrams. By introducing Multi-valued decision diagrams (MDDs) , tools were able to represent integral and real-valued functions, thus enhancing the applications of symbolic strategies to formal verification. In recent years, the LTSmin tool \cite{KantLMPBD15} developed by the University of Twente employs the SYLVAN multi-core MDDs library \cite{DijkP17} to speed up symbolic analysis algorithms for CTL model checking. A different solution was adopted by an extended version of SMV, NuSMV \cite{CimattiCGGPRST02}, which mantained the specification language of McMillan's tool while improving it by introducing LTL model checking and Sat-based Bounded model checking \cite{BiereCCZ99}, which exploits propositional satisfiability without using BDDs to represent the state graph. This approach was chosen because working with decision diagrams does not always guarantee an improvement over explicit model checking tecniques due to the often time-consuming procedure of selecting a variable ordering for all variables in the system, which is a known NP-complete problem \cite{BolligW96}.

Until the present day, our GreatSPN framework used multi-valued, multi-terminal decision diagrams (MTMDDs) provided by the Meddly library \cite{BabarM10} to perform CTL model checking on Petri Nets \cite{BabarBDM10}. Meddly is possibly the only open-source library to implement MTMDDs, Edge-valued MDDs (EVMDDs) while providing state-of-the-art algorithms to manipulate them. To determine the optimal variable ordering for the MDDs used to represet the state graph, GreatSPN uses a set of algorithms based on different heuristics which are run during the state space generation procedure \cite{AmparoreDBGM17}. As we are going to discuss later in this dissertation, GreatSPN is now capable of CTL* model checking by reducing symbolic LTL model checking to CTL model checking with fairness constraints, as demonstrated in a notorious article \cite{ClarkeGH97} by Clarke et al.

Background

Linear Temporal Logic

LTL is a propositional temporal logic with linear time model, meaning that it considers a single realized future behavior of a system, that is, a single path in a Kripke structure.

Syntax of LTL. The formal syntax of LTL is given by the following grammar in Backus-Naur form (BNF), where a ∈ AP is an atomic proposition.

ɸ ::= true | a | ¬ɸ | ɸ ∧ ɸ | Xɸ | ɸ U ɸ

Using boolean connectors such as ¬ and ∧ allows LTL to be treated as a propositional logic. Other boolean connectives such as disjunction ∨, implication →, equivalence ↔ and the exclusive or (xor) operator ⊕ can be derived as for any other propositional logic. This LTL grammar is defined using two basic temporal modalities: X (next) and U (until). Using those, we can derive two essential temporal modalities F (eventually) and G (always), as follows:

Fɸ = true\textbf{U}ɸ
Gɸ = ¬\textbf{F}¬ɸ

We now present a list of the temporal modalities which will be used at a later time in this dissertation.

• Gɸ: "always" (now and forever in the future ɸ is true)
• Fɸ: "eventually" (eventually in the future ɸ is true)
• Xɸ: "next" (in the next time step ɸ is true)
• ψ\textbf{U}ɸ: "until" (ψ is true until ɸ is true)

By combining the aforementioned temporal operators we obtain other, more complex modalities. A typical example is the specification which requires a property to be true infinitely often, GFɸ.

¶graph{LTL Semantics} LTL semantics is defined for infinite words σ over the alphabet 2\textsuperscript{AP}. The satisfiability rules are shown below:

• \(\sigma \vDash true\)
• \(\sigma \vDash a\) iff \(a \in A_{0}\)
• \(\sigma \vDash \phi_{1} \wedge \phi_{2}\) iff \(\sigma \vDash \phi_{1}\) and \(\sigma \vDash \phi_{2}\)
• \(\sigma \vDash \neg\phi\) iff \(\neg (\sigma \vDash \phi)\)
• \(\sigma \vDash \textbf{X}\phi\) iff \(\sigma[1...] \vDash \phi\)
• \(\sigma \vDash \phi_{1}\textbf{U}\phi_{2}\) iff \(\exists j \geq 0, \sigma[j...] \vDash \phi_{2}\) and \(\sigma[i...] \vDash \phi_{1}\) for all \(0 \leq i < j\)

A LTL formula ɸ is said to be valid with regard to a Kripke structure M if it holds for all paths of M. It is satisfiable if it holds for some path in M.

CTL*

We briefly introduced CTL* while dealing with the shortcomings of LTL and CTL. CTL* is a branching temporal logic which extends CTL following a proposal by Emerson and Halpern. Being based on the concept of branching time, CTL* is able to represent the possibility of existence of a determinate behavior in a tree of execution, using CTL path quantifiers E (for some path) and A (for all paths) to specify whether the required behavior must be verified for some execution of our system or all possible ones.

CTL* allows path quantifiers to be arbitrarely nested with linear temporal operators G, F, X and U. In contrast, CTL only supports linear temporal operators if they are immediately preceded by a path quantifier. In a similar fashion as CTL, the syntax of CTL* distinguishes between state and path formulae. CTL* path formulae are defined as LTL formulae, whith the only difference that here state formulae can be used as atoms.

Syntax of CTL*. The formal syntax of CTL* is made of state formulae Φ and path formulae ɸ. The syntax of CTL* state formulae Φ is defined over the set AP of atomic propositions:

Φ ::= true | a | ¬ɸ | ɸ ∧ ɸ | Eɸ

The syntax of CTL* path formulae ɸ is given by the following grammar, where Φ is a state formula:

ɸ ::= Φ | ¬ɸ | ɸ ∧ ɸ | Xɸ | ɸ U ɸ

As previously seen for LTL, the syntax of CTL* can be treated as any propositional logic, therefore all boolean connectives can be derived from ¬ and ∧. The missing temporal modalities F and G descend from X and U as it was the case for LTL, while the path quantifier A can be obtained from the following equivalence:

Aɸ = ¬\textbf{E}¬ɸ

¶graph{CTL* Semantics} Let a ∈ AP be an atomic proposition, $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, state s ∈ S, Φ and Ψ be CTL* state formulae and ɸ, ɸ\textsubscript{1} and ɸ\textsubscript{2} be CTL* path formulae.

¶graph{State formulae: semantics}

• \(s \vDash a\) iff \(a \in \textit{L(s)}\)
• \(s \vDash \Phi \wedge \Psi\) iff \(s \vDash \Phi\) and \(s \vDash \Psi\)
• \(s \vDash \neg\Phi\) iff \(\neg (s \vDash \Phi)\)
• \(s \vDash \textbf{E}\phi\) iff \(\sigma \vDash \phi\) for some \(\sigma \in \textit{Paths(s)}\)

¶graph{Path formulae: semantics}

• \(\sigma \vDash \Phi\) iff \(s_{0} \vDash \Phi\)
• \(\sigma \vDash \phi_{1} \wedge \phi_{2}\) iff \(\sigma \vDash \phi_{1}\) and \(\sigma \vDash \phi_{2}\)
• \(\sigma \vDash \neg\phi\) iff \(\neg (\sigma \vDash \phi)\)
• \(\sigma \vDash \textbf{X}\phi\) iff \(\sigma[1...] \vDash \phi\)
• \(\sigma \vDash \phi_{1}\textbf{U}\phi_{2}\) iff \(\exists j \geq 0, \sigma[j...] \vDash \phi_{2}\) and \(\sigma[i...] \vDash \phi_{1}\) for all \(0 \leq i < j\)

Decision Diagrams

Decision diagrams are directed, acyclic graphs used to represent functions over variables with finitely many possible assignments. They were originally studied by Bryant \cite{Bryant86} as a representation of boolean functions in the form of Binary Decision Diagrams (BDDs). We focus on a generalization of BDDs called Multi-value Decision Diagrams (MDDs) \cite{MDD}, whose variable domain can be arbitrarely large and which can be used to represent functions of integral and real-valued variables.

Multi-valued Decision Diagram. A multi-valued desicion diagram, or MDD, is an acyclic graph in which each node represents a function over variables with finitely many possible assignments, of the form:

$f : S_{K} \times ... \times S_{1} \rightarrow \{ 0, \ldots, m - 1 \}$

Each one of the sets $S_{k}$ is considered to be finite on an arbitrarely large domain. We can write:

$S_{k} = \{ 0, 1, \ldots, n_{k} - 1 \}$

An MDD is composed of two types of nodes: terminal nodes and non-terminal nodes.

• Terminal nodes are labeled with values from the set $\{0,1,\ldots,m-1\}$, representing the constant function:

$g (x_{K},\ldots,x_{1}) = a$

• Non-terminal nodes are labeled with one of the function variables $x_{k}$ and contain $n_{k}$ arcs to other nodes.

A non terminal node labeled with $x\textsubscript{k}$ has an outgoing arc corresponding to value $v$ which goes to a node representing the function:

$f_{x_{k}=v}(x_{K},\ldots,x_{1}) \equiv f(x_{K},\ldots,x_{k+1},v,x_{k-1},\ldots,x_{1})$

¶graph{Reduced ordered MDDs} In the contest of model checking, MDDs are useful to encode the state space of a model as a boolean, integral or real-valued function. To fit this purpose, MDDs must be in canonical form, meaning that for any given function and variable ordering, there must be exactly one representation of that function as MDD. For this to be true, we have to impose two constraints on MDDs: that they are ordered and reduced (ROMDDs).

Ordered MDDs. An MDD is ordered if all paths through the MDD visit non-terminal nodes accortding to the same variable ordering.

Reduced Ordered MDDs. A reduced, ordered MDD is an ordered MDD that contains no duplicate nodes and no redundant nodes.

• Two nodes are redundant if all of its outgoing arcs point to the same node.
• Two terminal nodes are duplicates if they have the same label, while two non-terminal nodes are duplicates if they have the same variable label and the same outgoing arcs for each value.

Automata over infinite words

We've described how Linear Temporal Logic provides a language to describe the temporal order of a series of events. When applied to formal verification, these sequences of events can be interpreted as computations of the program. A computation is a potentially infinite sequence of program states: each state is described by a finite set of atomic propositions, which will be referred to as a nonempty alphabet. Therefore a computation can be treated as an infinite word over the alphabet of truth assignments to the atomic propositions of a given alphabet.

This reasoning suggests that a LTL specification can be thought of as a description of a language over some alphabet. This language is made of infinite words, which represent program computations. We can exploit this equivalence of computations and words to connect linear temporal logic to automata theory applied on infinite words. As we are going to show, automata over infinite words depict a suitable formalism to represent LTL specifications. More precisely, given any propositional temporal formula, one can construct a finite automaton over infinite words that accepts precisely the computations satisfied by the formula \cite{VardiW94}. This chapter will present an introduction to automata theory and describe how LTL model checking employs a particular class of automata over infinite words, called Büchi automata.

\bibliographystyle{/usr/share/texmf-dist/bibtex/bst/base/acm} \bibliography{tesi}