The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques to verify systems.

Security protocols stipulate how the remote principals of a computer network should interact in order to obtain specific security goals. The crucial goals of confidentiality and authentication may be achieved in various forms, each of different strength. Using soft (rather than crisp) constraints, we develop a uniform formal notion for the two goals. They are no longer formalised as mere yes/no properties as in the existing literature, but gain an extra parameter, the security level. For example, different messages can enjoy different levels of confidentiality, or a principal can achieve different levels of authentication with different principals. The goals are formalised within a general framework for protocol analysis that is amenable to mechanisation by model checking. Following the application of the framework to analysing the asymmetric Needham-Schroeder protocol (Bella and Bistarelli 2001; Bella and Bistarelli 2002), we have recently discovered a new attack on that protocol as a form of retaliation by principals who have been attacked previously. Having commented on that attack, we then demonstrate the framework on a bigger, largely deployed protocol consisting of three phases, Kerberos.

The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear logic programming language called LO (Andreoli and Pareschi, 1990) enriched with universally quantified goal formulas. Although LO was originally introduced as a theoretical foundation for extensions of logic programming languages, it can also be viewed as a very general language to specify a wide range of infinite-state concurrent systems (Andreoli, 1992; Cervesato, 1995). Our approach is based on the relation between backward reachability and provability highlighted in our previous work on propositional LO programs (Bozzano et al., 2002). Following this line of research, we define here a general framework for the bottom-up. evaluation of first order linear logic specifications. The evaluation procedure is based on an effective fixpoint operator working on a symbolic representation of infinite collections of first order linear logic formulas. The theory of well quasi-orderings Abdulla et al., 1996; Finkel and Schnoebelen, 2001) can be used to provide sufficient conditions for the termination of the evaluation of non trivial fragments of first order linear logic.

The ability of providing and relating temporal representations at different ‘grain levels’ of the same reality is an important research theme in computer science and a major requirement for many applications, including formal specification and verification, temporal databases, data mining, problem solving, and natural language understanding. In particular, the addition of a granularity dimension to a temporal logic makes it possible to specify in a concise way reactive systems whose behaviour can be naturally modeled with respect to a (possibly infinite) set of differently-grained temporal domains. Suitable extensions of the monadic second-order theory of $k$ successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the monadic second-order theories of downward unbounded layered structures, which are infinitely refinable structures consisting of a coarsest domain and an infinite number of finer and finer domains, and of upward unbounded layered structures, which consist of a finest domain and an infinite number of coarser and coarser domains, with expressively complete and elementarily decidable temporal logic counterparts. We obtain such a result in two steps. First, we define a new class of combined automata, called temporalized automata, which can be proved to be the automata-theoretic counterpart of temporalized logics, and show that relevant properties, such as closure under Boolean operations, decidability, and expressive equivalence with respect to temporal logics, transfer from component automata to temporalized ones. Then, we exploit the correspondence between temporalized logics and automata to reduce the task of finding the temporal logic counterparts of the given theories of time granularity to the easier one of finding temporalized automata counterparts of them.

A system is data-independent with respect to a data type $X$ iff the operations it can perform on values of type $X$ are restricted to just equality testing. The system may also store, input and output values of type $X$. We study model checking of systems which are data-independent with respect to two distinct type variables $X$ and $Y$, and may in addition use arrays with indices from $X$ and values from $Y$. Our main interest is the following parameterised model-checking problem: whether a given program satisfies a given temporal-logic formula for all non-empty finite instances of $X$ and $Y$. Initially, we consider instead the abstraction where $X$ and $Y$ are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the $\mu$-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of $X$ and $Y$. We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the $\mu$-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the $\mu$-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where $X$ is the type of memory addresses, and $Y$ the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.

We propose an alternative way to represent graphs via OBDDs based on the observation that a partition of the graph nodes allows sharing among the employed OBDDs. In the second part of the paper we present a method to compute at the same time the quotient w.r.t. the maximum bisimulation and the OBDD representation of a given graph. The proposed computation is based on an OBDD-rewriting of the notion of Ackermann encoding of hereditarily finite sets into natural numbers.

We present a new approach to termination analysis of numerical computations in logic programs. Traditional approaches fail to analyse them due to non well-foundedness of the integers. We present a technique that allows overcoming these difficulties. Our approach is based on transforming a program in a way that allows integrating and extending techniques originally developed for analysis of numerical computations in the framework of query-mapping pairs with the well-known framework of acceptability. Such an integration not only contributes to the understanding of termination behaviour of numerical computations, but also allows us to perform a correct analysis of such computations automatically, by extending previous work on a constraint-based approach to termination. Finally, we discuss possible extensions of the technique, including incorporating general term orderings.