In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.

We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.

We develop a sound, complete, and practically implementable tableau-based decision method for constructive satisfiability testing and model synthesis for the fragment ATL + of the full alternating-time temporal logic ALT * . The method extends in an essential way a previously developed tableau-based decision method for ATL and works in 2EXPTIME, which is the optimal worst-case complexity of the satisfiability problem for ATL + . We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL + formulas can reduce the complexity of the satisfiability problem.

We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely Gentzen sequent calculus for minimal logic. Our calculus is inspired by the Curry-Howard isomorphism, in the sense that types, both for patterns and terms, correspond to propositions, terms correspond to proofs, and term reduction corresponds to sequent proof normalization performed by cut elimination. The calculus enjoys subject reduction, confluence, preservation of strong normalization w.r.t. a system with meta-level substitutions and strong normalization for well-typed terms. As a consequence, it can be seen as an implementation calculus for functional formalisms defined with meta-level operations for pattern matching and substitutions.

The aim of this paper is to propose linear logic as a proof system allowing one to perform updates of databases containing incomplete information. In our approach, a database is specified by facts, deduction rules (among which default rules) and update constraints. Updates will always preserve consistency, i.e. any update of a ‘consistent’ database will produce a new base which is ‘consistent’. The computation of the ‘static semantics’ of a database DB corresponds to the construction of a proof in a logical theory associated to the database; the non logical axioms of such a theory are linear sequents formalising the deduction rules and the update constraints of DB. Similarly, the calculus of the ‘update semantics’ of a database DB w.r.t. the insertion of a literal L, is the construction of a proof in the very same linear theory.

A declarative semantics for the class of allowed logic programs is proposed. Such a semantics is a logical theory, the linear completion of the program P, which differs from Clark's completion because the underlying logic is linear logic rather than classical logic. With respect to such a semantics, the soundness and completeness of SLDNF-resolution is proven. That is, it is proven that the computational notion of success of an allowed query Q for an allowed program P corresponds to the provability of an instantiation of Q in the linear completion of P, and the notion of failure to the provability of the (linear) negation of Q in the linear completion of P.>