1: \section{Introduction}
2:
3: Recently, a novel paradigm for applying declarative logic
4: programming techniques has been proposed.
5: In this approach, called \emph{answer set programming}
6: (a term coined by Vladimir Lifschitz), a problem
7: is solved by devising a logic program such that models
8: of the program provide the answers to the
9: problem~\cite{Lifschitz99:iclp,MT99:slp,Niemela99:amai}.
10: Much of this work has been based on the stable model
11: semantics~\cite{GL88} and there are
12: %fairly
13: efficient systems
14: %such as
15: \dlv\ (\url{http://www.dbai.tuwien.ac.at/proj/dlv/}) and
16: \Smodels\ (\url{http://www.tcs.hut.fi/Software/smodels/})
17: for computing stable\linebreak
18: models of logic programs.
19: Using such an answer set programming system a problem is solved by
20: writing a logic program whose stable models capture the solutions of the
21: problem and then employing the system to compute a solution, i.e., a stable
22: model.
23:
24: In this paper we put forward symbolic model
25: checking~\cite{Burch92,CGP99:book} as a promising application area for
26: answer set programming systems. In particular, we demonstrate how
27: bounded model checking problems of asynchronous concurrent systems can
28: be reduced to computing stable models of logic programs.
29:
30: Verification of asynchronous systems is typically done by enumerating
31: the reachable states of the system.
32: Tools based on this approach (with various
33: enhancements) include, e.g., the \textsc{Spin} system~\cite{Holzmann97},
34: which supports extended finite state machines communicating through FIFO
35: queues, and the Petri net model based \textsc{PROD} tool~\cite{PROD32}.
36: The main problem with enumerative model checkers is the
37: amount of memory needed for the set of reachable states.
38:
39: Symbolic model checking is widely applied especially in hardware
40: verification. The main analysis technique is based on (ordered) binary
41: decision diagrams (BDDs). In many cases the set of reachable states
42: can be represented very compactly using a BDD encoding.
43: Although the approach has been successful,
44: there are difficulties in applying BDD-based techniques, in particular,
45: in areas outside hardware verification. The key problem is that some
46: Boolean functions do not have a compact representation as BDDs and the
47: size of the BDD representation of a Boolean function is very sensitive
48: to the variable ordering.
49: %
50: Bounded model checking~\cite{BiereCimattiClarkeZhu:TACAS1999} has been
51: proposed as a technique for overcoming the space problem by replacing
52: BDDs with satisfiability (SAT) checking techniques because typical SAT checkers use only
53: polynomial amount of memory. The idea is roughly the following. Given a
54: sequential digital circuit, a (temporal) property to be verified, and a bound $n$,
55: the behaviour of a sequential circuit is unfolded up to $n$ steps as a
56: Boolean formula $S$ and the negation of the property to be verified is
57: represented as a Boolean formula $\overline{R}$. The translation to Boolean
58: formulas is done so that $S \land \overline{R}$ is satisfiable iff the system has a
59: behaviour violating the property of length at most~$n$.
60: Hence, bounded
61: model checking provides directly interesting and practically relevant
62: benchmarks for any answer set programming system capable of handling
63: propositional satisfiability problems.
64:
65: Until now bounded model checking has been applied to synchronous
66: hardware verification and little attention has been given to knowledge
67: representation issues such as developing concise and efficient logical
68: representation of system behaviour.
69: In this work we study the knowledge representation problem
70: and employ ideas used in reducing planning to stable model
71: computation~\cite{Niemela99:amai}.
72: The aim is to develop techniques such that the behaviour of an
73: asynchronous concurrent system can be encoded compactly and the
74: inherent concurrency in the system could be exploited in model checking
75: the system.
76: %
77: To illustrate the approach we use
78: a simple basic Petri net model of asynchronous systems,
79: 1-safe Place/Transition nets (P/T nets), which is an interesting
80: generalisation of communicating automata~\cite{DeselReisig:PT}.
81: Thus properties of finite state systems composed of finite state
82: machine components can be verified using model checkers for 1-safe Petri nets.
83:
84:
85: The structure of the rest of the paper is the following. In the next
86: section we introduce Petri nets and the bounded model checking problem.
87: Then we develop a compact encoding of bounded
88: model checking as the problem of finding stable models of logic
89: programs.
90: We first show how to treat reachability properties such as
91: deadlocks
92: and then demonstrate how to extend the approach to cope with properties
93: expressed in linear temporal logic (LTL).
94: We discuss initial experimental results and end with some concluding
95: remarks.
96:
97: \section{Petri nets and bounded model checking}
98: \begin{figure}
99: \begin{center}
100: \epsfig{file=running.eps,width=65mm}
101: \caption{Running Example}
102: \label{fig:running}
103: \end{center}
104: \end{figure}
105:
106: There are several Petri net derived models presented in the literature.
107: We will use P/T-nets which are one of the simplest forms of Petri nets.
108: We will use as a running example the P/T-net presented in
109: Fig.~\ref{fig:running}.
110:
111: A triple $\seq{P, T, F}$ is a {\em net} if $P \cap T = \emptyset$ and
112: $F \subseteq (P \times T) \cup (T \times P)$. The elements of $P$
113: are called {\em places}, and the elements of $T$ {\em transitions}. Places
114: and transitions are also called {\em nodes}.
115: The places are represented in graphical notation by circles,
116: transitions by squares, and the {\em flow relation} $F$ by arcs.
117: %
118: We identify $F$ with its characteristic function on the set
119: $(P \times T) \cup (T \times P)$.
120: The {\em preset} of a node $x$,
121: denoted by ${}^{\bullet}x$, is the set
122: $\{y \in P \cup T \, \arrowvert \, F(y, x) = 1\}$.
123: In our running example, e.g., ${}^{\bullet}t2 = \{ p1, p2 \}$.
124: The {\em postset} of a node $x$,
125: denoted by $x^{\bullet}$, is the set
126: $\{y \in P \cup T \, \arrowvert \, F(x, y) = 1\}$.
127: Again in our running example
128: $p2^{\bullet} = \{ t2, t3, t5\}$.
129:
130: A {\em marking} of a net $\seq{P, T, F}$ is a mapping $P \mapsto \bbbn$.
131: A marking $M$ is identified with the multi-set which contains $M(p)$
132: copies of $p$ for every $p \in P$.
133: A 4-tuple $\Sigma = \seq{P, T, F, M_0}$ is a {\em net system} (also
134: called a {\em P/T-net}) if
135: $\seq{P, T, F}$ is a net and $M_0$ is a marking of $\seq{P, T, F}$
136: called the {\em initial marking}.
137: A marking is graphically denoted by a distribution of tokens on
138: the places of the net. In our running example in
139: Fig.~\ref{fig:running} the net has the initial marking
140: $M_0 = \{ p1, p2 \}$.
141:
142: A marking $M$ enables a transition $t \in T$ if
143: $\forall p \in P: F(p,t) \leq M(p)$. If $t$ is enabled, it can {\em occur}
144: leading to a new marking (denoted $M \overset{t}{\rightarrow} M^{\prime}$),
145: where $M^{\prime}$ is
146: defined by $\forall p \in P: M^{\prime}(p) = M(p) - F(p,t) + F(t,p)$.
147: In the running example $t2$ is enabled in the initial
148: marking $M_0$, and thus $M_0 \overset{t2}{\rightarrow} M^{\prime}$, where
149: $M^{\prime} = \{ p3, p4 \}$.
150: A~marking $M$ is a {\em deadlock} if no transition $t \in T$ is enabled by $M$.
151: In our running example the marking $M = \{p1, p5\}$ is a deadlock.
152:
153: A marking $M_n$ is {\em reachable} in $\Sigma$ if there is an {\em
154: execution}, i.e., a (possibly empty) sequence of transitions $t_0, t_1, \ldots, t_{n-1}$
155: and markings $M_1, M_2, \ldots, M_{n-1}$ such that:
156: $M_0 \overset{t_{0}}{\rightarrow} M_1 \overset{t_{1}}{\rightarrow} \ldots M_{n-1} \overset{t_{n-1}}{\rightarrow} M_{n}$.
157: A marking $M$ is reachable within a bound $n$, if
158: there is an execution with at most $n$ transitions, with which
159: $M$ is reachable.
160: The~net system may also have {\em infinite executions},
161: i.e., infinite sequences of transitions $t_0, t_1, \ldots$
162: and markings $M_1, M_2, \ldots$ such that:
163: $M_0 \overset{t_{0}}{\rightarrow} M_1 \overset{t_{1}}{\rightarrow} \ldots$.
164: The {\em maximal executions} of a net system are the
165: infinite executions of the net system together with the (finite) executions
166: leading to a deadlock marking.
167:
168: A marking $M$ is 1-safe if $\forall p \in P: M(p) \leq 1$.
169: A P/T-net is 1-safe if all its reachable markings are 1-safe.
170: We will restrict ourselves to finite P/T-nets which are 1-safe,
171: and in which each transition has both nonempty pre- and
172: postsets.
173:
174: Given a 1-safe P/T-net $\Sigma$, we say that a set
175: of transitions $S \subseteq T$ is {\em concurrently enabled} in the marking $M$, if
176: (i) all transitions $t \in S$ are enabled in $M$, and (ii)
177: for all pairs of transitions $t, t^{\prime} \in S$, such that $t \not = t^{\prime}$,
178: it holds that ${{}^{\bullet}t} \cap {{}^{\bullet}t^{\prime}} = \emptyset$.
179: If a set $S$ is concurrently enabled in the marking $M$, it can be fired
180: in a {\em step} (denoted $M \overset{S}{\rightarrow} M^{\prime}$),
181: where $M^{\prime}$ is the marking reached after firing all of the transitions
182: in the step $S$ in arbitrary order. It is easy to prove by using the 1-safeness
183: of the P/T-net $\Sigma$ that all possible interleavings of transitions in a step
184: $S$ are enabled in $M$, and that they all lead to the same final marking $M^{\prime}$.
185: In our running example in the marking $M^{\prime} = \{ p3, p4 \}$ the step
186: $\{ t1, t4 \}$ is enabled, and will lead back to the initial marking $M_0$. This
187: is denoted by $M^{\prime} \overset{\{ t1, t4 \}}{\rightarrow} M_0$.
188: Notice also that for any enabled transition, the singleton set containing only
189: that transition is
190: a step.
191:
192: We say that a
193: marking $M_n$ is {\em reachable in step semantics} in a 1-safe P/T-net
194: if there is a {\em step execution}, i.e., a (possibly empty) sequences
195: $S_0, S_1, \ldots, S_{n-1}$ of steps
196: and $M_1, M_2, \ldots, M_{n-1}$ of markings such that:
197: $M_0~\overset{S_{0}}{\rightarrow}~M_1~\overset{S_{1}}{\rightarrow}~\ldots
198: M_{n-1}~\overset{S_{n-1}}{\rightarrow}~M_{n}$.
199: A~marking $M$ is reachable within a bound $n$ in the step semantics, if
200: there is a step execution with at most $n$ steps, with which
201: $M$ is reachable.
202: We will refer to the ``normal semantics''
203: as {\em interleaving semantics}.
204: The {\em infinite step executions} and {\em maximal step executions}
205: are defined in a similar way as in the interleaving case.
206:
207: Note that if a marking is reachable in
208: $n$ transitions in the interleaving semantics, it is also reachable
209: in $n$ steps in the step semantics. However, the converse does not
210: necessarily hold.
211: We have, however, the following theorem which implicitly follows from the
212: results of~\cite{BD:TCS87}.
213: \begin{theorem}
214: For finite 1-safe P/T-nets the set of reachable markings in
215: the interleaving and step semantics coincide.
216: \end{theorem}
217:
218: \paragraph{Linear temporal logic (LTL).}
219: The linear temporal logic LTL is one of the most widely used logics for
220: model checking reactive systems,
221: see e.g., \cite{CGP99:book}.
222: The basic idea is to specify properties that the system should have using
223: LTL.
224: A~model checker is then used to check whether all behaviours of the system
225: are models of the specification formula. If not, then the model checker
226: outputs a behaviour of the system which violates the given specification.
227:
228: Given a finite set $AP$ of atomic propositions,
229: the syntax of LTL
230: is given by:
231: \[ \varphi ::=
232: p \in AP \,\, \arrowvert \,\,
233: \neg \varphi_{1} \,\, \arrowvert \,\,
234: \varphi_{1} \, \vee \, \varphi_{2} \,\, \arrowvert \,\,
235: \varphi_{1} \, \wedge \, \varphi_{2} \,\, \arrowvert \,\,
236: \varphi_{1} \, U \, \varphi_2 \,\, \arrowvert \,\,
237: \varphi_{1} \, R \, \varphi_2 \; .
238: \]
239: Note that we do not define the often used
240: next-time operator $X \, \varphi_{1}$.
241: This is a commonly used tradeoff which in our case allows the combination of the step
242: semantics with LTL model checking.
243:
244: We use $V = 2^{AP}$ as our alphabet.
245: We denote by $V^{+}$ all finite sequences over $V$ excluding the empty sequence,
246: and with $V^{\omega}$ all infinite sequences over $V$.
247: A word $w \in V^{+} \cup V^{\omega}$
248: is thus either a finite sequence $w = x_0\,x_1\,\ldots\, x_n$
249: or an infinite sequence $w = x_0\,x_1\,\ldots$, such that
250: $x_i \in V$ for all $i \geq 0$.
251: For a word $w$ we define $w_{(i)} = x_i$, and denote by
252: $w^{(i)}$ the suffix of $w$ starting at $x_i$.
253: When $w \in V^{+}$ we
254: define $|w|$ to be the length of the word $w$, and
255: in the case $w \in V^{\omega}$ we define $|w| = \omega$
256: where $\omega$ is greater than any natural number.
257:
258: The relation $w \models \varphi$ is defined inductively as follows:
259: \begin{itemize}
260: \item $w \models p$ iff $p \in w_{(0)}$ for $p \in AP$,
261: \item $w \models \neg \varphi_{1}$ iff not $w \models \varphi_{1}$,
262: \item $w \models \varphi_{1} \, \vee \, \varphi_{2}$ iff
263: $w \models \varphi_{1}$ or $w \models \varphi_{2}$,
264: \item $w \models \varphi_{1} \, \wedge \, \varphi_{2}$ iff
265: $w \models \varphi_{1}$ and $w \models \varphi_{2}$,
266: \item $w \models \varphi_{1} \, U \, \varphi_2$ iff there exists
267: $0 \leq j < |w|$, such that
268: $w^{(j)} \models \varphi_{2}$ and
269: for all $0 \leq i < j$, $w^{(i)} \models \varphi_{1}$,
270: \item $w \models \varphi_{1} \, R \, \varphi_2$ iff for all
271: $0 \leq j < |w|$,
272: if for every $0 \leq i < j$
273: $w^{(i)} \not \models \varphi_{1}$
274: then $w^{(j)} \models \varphi_{2}$ .
275: \end{itemize}
276: We define some shorthand LTL formulas:
277: $\top \equiv p \, \vee \, \neg p$ for some arbitrary fixed $p \in AP$,
278: $\bot \equiv \neg \top$,
279: $\Diamond \, \varphi \equiv (\top \, U \, \varphi)$,
280: $\Box \, \varphi \equiv (\bot \, R \, \varphi)$,
281: and $\varphi_1 \rightarrow \varphi_2 \equiv \neg \varphi_1 \vee \varphi_2$.
282: The temporal operators are called: $U$ for ``until'', $R$ for ``release'',
283: $\Diamond$ for ``eventually'',
284: and $\Box$ for ``globally''.
285: %
286: Our definition of the semantics of LTL above is somewhat redundant.
287: This was done on purpose, as we often in this work use LTL formulas in
288: {\em positive normal form}, in which only a restricted use of
289: negations is allowed.
290: To be more specific,
291: an LTL formula is said to be in
292: positive normal form when all negations
293: in the formula appear directly before an atomic proposition.
294: A~formula can be put into positive normal form with
295: the following equivalences (and their duals):
296: $\neg \neg \varphi \equiv \varphi$,
297: $\neg (\varphi_1 \, \vee \, \varphi_2) \equiv \neg \varphi_1 \, \wedge \, \neg \varphi_2$,
298: and
299: $\neg (\varphi_1 \, U \, \varphi_2) \equiv \neg \varphi_1 \, R \, \neg \varphi_2$.
300: Note that converting a formula into positive normal form does not
301: involve a blowup.
302:
303: Some examples of practical use of LTL formulas
304: are:
305: $\Box \neg(\mathit{cs}_1 \wedge \mathit{cs}_2)$ (it always holds that two processes are
306: not at the same time in a critical section),
307: $\Box (\mathit{req} \rightarrow \Diamond \mathit{ack})$
308: (it is always the case that a request is eventually followed by an acknowledgement),
309: and
310: $((\Box \Diamond \mathit{sch}_1) \wedge (\Box \Diamond \mathit{sch}_2)) \rightarrow (\Box (\mathit{tr}_1 \rightarrow \Diamond \mathit{cs}_1))$
311: (if both process 1 and 2 are scheduled infinitely often, then
312: always the entering of process 1 in the trying section
313: is followed by the process 1 eventually entering
314: the critical section).
315:
316: Given a 1-safe P/T net $\Sigma$, we use a chosen subset of the places
317: as the atomic propositions $AP$.
318: A maximal (interleaving) execution
319: $M_0 \newarrow{t_0}M_1\newarrow{t_1}\ldots$ satisfies~$\varphi$ iff
320: the corresponding word
321: $w = (M_0 \cap AP), (M_1 \cap AP), \ldots$ satisfies $\varphi$. We say that
322: $\Sigma$ satisfies $\varphi$ iff every maximal execution starting
323: from the initial marking $M_0$ satisfies~$\varphi$.
324: Alternatively, $\Sigma$
325: does not satisfy $\varphi$ if there exists a maximal execution starting
326: from $M_0$ which satisfies $\neg \varphi$.
327: We call such an execution a {\em counterexample}.
328: Notice that we restrict ourselves to maximal executions
329: and thus our counterexamples are either infinite executions
330: or finite executions
331: leading to a deadlock (recall the
332: definition of maximal executions).
333:
334: The temporal logic LTL can specify quite complex
335: properties of reactive systems.
336: In many cases it suffices to reason about much simpler temporal
337: properties. A~typical example is the reachability of a marking satisfying
338: some condition $C$ which in the LTL setting
339: corresponds to finding a counterexample for a formula $\Box \neg C$.
340: An important reachability based problem is deadlock detection.
341: \begin{definition}
342: {\bf(Deadlock detection)} Given a 1-safe P/T-net $\Sigma$, is there
343: a reachable marking $M$ which does not enable any transition
344: of $\Sigma$?
345: \end{definition}
346:
347: Most analysis questions including deadlock detection and LTL model checking
348: are PSPACE-complete in the size of a 1-safe Petri net,
349: see e.g.,~\cite{Esparza:thumb}. In {\em bounded model checking} we
350: fix a bound $n$ and look for counterexamples which are
351: shorter than the given bound $n$.
352: For example,
353: in the case of {\em bounded deadlock detection} we look
354: for executions reaching a deadlock in at most $n$ transitions.
355: It is easy to show that, e.g.,
356: the bounded deadlock detection problem
357: is NP-complete (when the bound $n$ is given in unary coding).
358: %
359: This idea can also be applied to LTL model checking.
360: In~\cite{BiereCimattiClarkeZhu:TACAS1999}
361: {\em bounded LTL model checking} is introduced.
362: They also discuss how to ensure that a given bound $n$ is
363: sufficient to guarantee completeness.
364: Unfortunately, getting an exact bound is often computationally infeasible,
365: and easily obtainable upper bounds are too large.
366: In the case of 1-safe P/T-nets they are exponential in the number of places in the net.
367: Therefore the bounded
368: model checking results are usually not conclusive if a
369: counterexample is not found. Thus bounded model checking is at its
370: best in ``bug hunting'', and not as easily applicable in verifying
371: systems to be correct.
372:
373: \input{bmc2asp}
374:
375: \subsection{Bounded LTL model checking}
376:
377: Our strategy for finding counterexamples for LTL formula $\varphi$
378: (i.e., executions satisfying $\neg \varphi$) is almost the same
379: as in \cite{BiereCimattiClarkeZhu:TACAS1999}. The main difference
380: is that we allow the system under model checking to have reachable
381: deadlocks, while their translation does not allow this.
382: This is also a difference to our previous work~\cite{HelNie:LPNMR2001}.
383:
384: Our counterexamples have two basic shapes.
385: On the left in Fig.~\ref{fig:cex} is
386: a {\em loop counterexample}, and on the right is a {\em counterexample without loop}.
387: \begin{figure}[thb]
388: \begin{center}
389: \input{paths.pstex_t}
390: \caption{Two counterexample possibilities}
391: \label{fig:cex}
392: \end{center}
393: \end{figure}
394: Loop counterexamples specify an infinite execution, while counterexamples
395: without a loop specify a~finite execution.
396: The arcs of the figure denote the ``next state'' of each state. Notice in the loop
397: counterexample that if $M_{(i-1)}$ is equivalent to the last state $M_n$, the state
398: $M_i$ is the ``next state'' of $M_n$.
399: The counterexamples without loop can additionally be divided into {\em deadlock executions}
400: (ending in a deadlock state), and {\em non-maximal executions} (ending in a state
401: which is not a deadlock).
402:
403: In the case of non-maximal executions our encoding is a cautious one,
404: and we will find counterexamples which exist, no matter how the
405: non-maximal execution is extended into a maximal one.
406: (Recall that we have defined the semantics of LTL over maximal executions of the
407: net system.) Finding non-maximal counterexample executions is in fact
408: only an optimisation. It was introduced in~\cite{BiereCimattiClarkeZhu:TACAS1999},
409: and allows some counterexamples to be found with smaller
410: bounds than would otherwise be possible.
411:
412: In the encoding we use the auxiliary atoms
413: $\mathit{el}(i), \mathit{le}, \mathit{nl}(i), \mathit{il}(i)$ with
414: following intuition (see Fig.~\ref{fig:cex} for an example).
415: The $\mathit{el}(i)$ atom is in a stable model for the state $i$ that is
416: equivalent with the last state $n$ and $\mathit{le}$ is in the model if
417: a loop exists, i.e., some $\mathit{el}(i)$ is in the model.
418: The $\mathit{nl}(i)$ atom is in a model for the
419: ``next state'' $i$ of the last state, while $\mathit{il}(i)$ is in the
420: model for all states $i$ in the loop.
421:
422: Given an LTL formula $f$ in positive normal form\footnote{
423: Using the positive normal form is required to handle non-maximal
424: counterexample executions, for which the duality
425: $f_1 \, R \, f_2 \equiv \neg (\neg f_1 \, U \, \neg f_2)$ can not be used,
426: see~\cite{BiereCimattiClarkeZhu:TACAS1999}.
427: }
428: (when the formula to be model checked is $\varphi$, the formula $f$ is
429: equivalent to $\neg \varphi$ with negations pushed in), and a bound $n
430: \geq 1$ we construct a program $\ltlprogram{f}{n}$ as follows.
431:
432:
433: \begin{itemize}
434: \item Guess which state is equivalent to the last (if any). For all $0 \leq i \leq n-1$ add rule
435: \begin{equation}
436: \{ \mathit{el}(i) \} \lparrow \; .\label{rule:guessloop}
437: \end{equation}
438: \item Disallow guessing two or more. (Guessing none is allowed though.) Add rule
439: \begin{equation}
440: \lparrow 2 \{ \mathit{el}(0), \mathit{el}(1), \ldots, \mathit{el}(n-1) \} \; .\label{rule:guesscheck}
441: \end{equation}
442: \item Check that the guess is correct. For all $0 \leq i \leq n-1$, $p \in P$ include rules
443: \begin{equation}
444: \lparrow \mathit{el}(i), p(i), \lpnot p(n) \hspace{2em}
445: \lparrow \mathit{el}(i), p(n), \lpnot p(i) \; .\label{rule:checkloop}
446: \end{equation}
447: \item Specify auxiliary loop related atoms.
448: For all $0 \leq i \leq n-1$, include rules
449: \begin{equation}
450: \mathit{le} \lparrow \mathit{el}(i) \hspace{1em}
451: \mathit{nl}(i+1) \lparrow \mathit{el}(i) \hspace{1em}
452: \mathit{il}(i+1) \lparrow \mathit{el}(i) \hspace{1em}
453: \mathit{il}(i+1) \lparrow \mathit{il}(i) \; .\label{rule:loopstuff}
454: \end{equation}
455: \item Require that if a loop exists, the last step contains a transition
456: to disallow looping by idling. Add the rule
457: \begin{equation}
458: \lparrow \mathit{le}, \mathit{idle}(n-1) \; .\label{rule:noidleloop}
459: \end{equation}
460: \item Allow at most one visible transition in a step to eliminate
461: steps which cannot be interleaved to yield a counterexample.
462: For all $0 \leq i \leq n-1$, add rule
463: \begin{equation}
464: \lparrow 2 \{ t_1(i), \ldots, t_k(i)\} \label{rule:onevisible}
465: \end{equation}
466: where $\{ t_1, \ldots, t_k \}$ is the set of {\em visible
467: transitions}, i.e.,
468: the transitions whose firing changes the marking of a place $p$ appearing in the formula $f$.
469: More formally, a transition $t \in T$ is visible, if there exists a place $p \in AP$
470: such that $F(t,p) - F(p,t) \not = 0$.
471: \end{itemize}
472: \input{\ltltrans}
473: We recursively translate the formula $f$ by first translating its subformulas,
474: and then $f$ as follows. For all $0 \leq i \leq n$, add the rules given
475: by Fig.~\ref{fig:trans}.\footnote{An equivalence explaining
476: the release translation:
477: $f_1 \, R \, f_2 \equiv (f_2 \, U \, (f_1 \, \wedge \, f_2 )) \, \vee \, (\Box f_2)$.}
478: Finally we require that the top level formula $f$ should hold in the initial marking
479: \begin{equation}
480: \lparrow \lpnot f(0) \; .\label{eq:topok}
481: \end{equation}
482: With this program $\ltlprogram{f}{n}$ we get our main result.
483: \begin{theorem}
484: \label{th:ltl}
485: Let $f$ be an LTL formula in positive normal form and
486: $N = \seq{P, T, F}$ be a 1-safe P/T-net for all initial markings
487: satisfying a condition $C_0$.
488: %
489: If $\mprogram{C_0}{0} \cup \aprogram{N}{n} \cup \lprogram{N}{n} \cup \ltlprogram{f}{n}$
490: has a stable model, then there is a maximal execution of
491: $N$ from an initial marking satisfying $C_0$ which satisfies~$f$.
492: \end{theorem}
493: \begin{proof}
494: See Appendix~\ref{app:ltl1}.
495: \end{proof}
496:
497: We also have the following completeness result for our translation.
498: First we define the notion of a {\em looping execution}.
499: A finite execution
500: $M_0 \overset{t_{0}}{\rightarrow} M_1 \overset{t_{1}}{\rightarrow} \ldots M_{n-1} \overset{t_{n-1}}{\rightarrow} M_{n}$ is a looping execution, if $n \geq 1$ and there exists an index $l < n$ such that $M_l = M_n$.
501: A looping execution together with the index $l$
502: is a finite witness to the existence of the corresponding (infinite) maximal execution $\sigma$ of the
503: net system $N$ which visits the sequence of states $M_0, M_1, \ldots, M_l, M_{l+1}, \ldots, M_k, M_{l+1}, \ldots, M_k, \ldots$.
504: \begin{theorem}
505: \label{th:compl}
506: Let $f$ be an LTL formula in positive normal form and
507: $N = \seq{P, T, F}$ be a 1-safe P/T-net for all initial markings
508: satisfying a condition $C_0$.
509: %
510: If $N$ has a looping or deadlock execution of at most length $n$
511: starting from an initial marking satisfying $C_0$ such that some corresponding
512: maximal execution $\sigma$ satisfies $f$, then
513: $\mprogram{C_0}{0} \cup \aprogram{N}{n} \cup \lprogram{N}{n} \cup \ltlprogram{f}{n}$
514: has a stable model.
515: \end{theorem}
516: \begin{proof}
517: See Appendix~\ref{app:compl}.
518: \end{proof}
519:
520:
521: The size of the program in Theorem~\ref{th:ltl} is linear in the size of the
522: net
523: and formula, i.e., ${\cal O}((\arrowvert P \arrowvert + \arrowvert T \arrowvert + \arrowvert F \arrowvert +
524: \arrowvert f \arrowvert) \cdot n)$.
525: The semantics of LTL is defined over interleaving executions.
526: A novelty of the translation is that it allows concurrency between
527: invisible transitions.
528:
529: We could simplify the LTL translation presented above
530: in following ways.
531: %
532: Firstly, if the net system is known to be deadlock free,
533: the release translation in Fig.~\ref{fig:trans} can be simplified by
534: removing the rule
535: $$f(n) \lparrow f_2(n), \lpnot \mathit{live},$$
536: and also the (now unnecessary) subprogram $\lprogram{N}{n}$.
537:
538: Secondly, if we remove
539: the possibility of obtaining non-maximal counterexample
540: executions, the release translation can be removed
541: fully by using the equivalence
542: $\varphi_{1} \, R \, \varphi_2 \equiv \neg \, (\neg \, \varphi_{1} \, U \, \neg \, \varphi_2)$
543: and adding (the obvious) translation for negation.
544: This can not be done when non-maximal counterexamples are
545: used, because the equivalence does not hold in that
546: case.
547: As an example, one can not deduce from the fact that
548: $\neg \Diamond \, \neg \, \varphi$ holds for a non-maximal execution $\sigma$
549: that $\Box \, \varphi$ holds for any maximal
550: execution $\sigma'$ such that $\sigma$ is a prefix of $\sigma'$.
551: The non-maximal counterexample executions are
552: quite valuable in practice, as using them violations to safety
553: properties can be found with smaller bounds.
554: Therefore we chose to use a more complicated
555: translation for release.
556:
557: \paragraph{Forcing interleaving semantics.}
558: We can create the interleaving semantics versions
559: of bounded model checking problems by adding
560: a set of rules $\iprogram{N}{n}$.
561: It includes for each time step
562: $0 \leq i \leq n-1$ a rule
563: \begin{equation}
564: \lparrow 2 \{ t_1(i), \ldots, t_m(i) \}
565: \label{eq:nostep}
566: \end{equation}
567: where $\{ t_1, \ldots, t_m \}$ is the set of all transitions.
568: These rules eliminate all stable models having more than one
569: transition firing in a step.
570: \begin{corollary}
571: Let $\sprogram{N}{n}$ be a program solving a bounded
572: model checking problem in the step semantics using any of
573: the translations above. Then the program
574: $\sprogram{N}{n} \cup \iprogram{N}{n}$ solves
575: the same problem in the interleaving semantics.
576: \end{corollary}
577:
578: \input{comparison}
579:
580: \input{experiments}
581:
582: \section{Conclusions}
583:
584: We introduce bounded model checking of asynchronous concurrent
585: systems modelled by 1-safe P/T-nets as an interesting application area for
586: answer set programming. We present mappings from bounded
587: reachability, deadlock detection, and LTL model checking problems of
588: 1-safe P/T-nets to stable model computation.
589: %
590: Our approach is capable of doing model checking for a set of initial
591: markings at once. This is usually difficult to achieve in current
592: enumerative model checkers and often leads to state space explosion.
593: We handle asynchronous systems using a step semantics whereas previous
594: work on bounded model checking only uses the interleaving
595: semantics~\cite{BiereCimattiClarkeZhu:TACAS1999}. Furthermore, our
596: encoding is more compact than the previous approach
597: employing propositional
598: satisfiability~\cite{BiereCimattiClarkeZhu:TACAS1999}.
599: This is because our rule based approach allows to represent executions
600: of the system, e.g.\ frame axioms, succinctly and supports directly the
601: recursive fixed point computation needed to evaluate LTL formulas.
602: Another feature of our LTL translation is that
603: it does not require the deadlock freeness
604: assumption used by~\cite{BiereCimattiClarkeZhu:TACAS1999},
605: and thus we can employ it also with systems which have not been
606: proved deadlock free.
607:
608: The first experimental results indicate that
609: stable model computation is quite a competitive approach to searching for
610: short executions of the system leading to deadlock and worth further
611: study.
612: %
613: More experimental work and comparisons are needed to determine the
614: strength of the approach. In particular, for comparing with SAT checking
615: techniques, it would be interesting to develop a similar treatment of asynchronous
616: systems using a SAT encoding and compare it to the logic program based
617: approach.
618:
619: Relating the net unfolding method
620: (see~\cite{Heljanko:Fundamenta99,MR:cav97} and further references there)
621: to bounded model checking would be interesting.
622: There are also alternative semantics to the
623: two presented in this work~\cite{Heljanko:Concur2001},
624: applying them to bounded LTL model checking is left for further work.
625:
626: