Search

Gödel's Dialectica interpretation was conceived as a tool to obtain the consistency of Heyting arithmetic in the 40s. In recent years, several proof theoretic transformations, based on Gödel's Dialectica interpretation, have been used systematically to extract new content from classical proofs, following a suggestion of Kreisel. Thus, the interpretation has found new relevant applications in several areas of mathematics and computer science. Several authors have explained the Dialectica interpretation in categorical terms. In particular, de Paiva introduced the notion of a Dialectica category as an internal version of Gödel's Dialectica Interpretation in her doctoral work. This was generalised by Hyland and Hofstra, who considered the interpretation in terms of fibrations. In our previous work, we introduced an intrinsic presentation of the Dialectica construction via a generalisation of Hofstra's work, using the notion of Gödel fibration and its proof-irrelevant version, a Gödel doctrine. The key idea is that Gödel fibrations (and doctrines) can be thought of as fibrations generated by some basic predicates playing the role of quantifier-free predicates. This categorification of quantifier-free predicates is crucial not only to show that our notion of Gödel fibration is equivalent to Hofstra's Dialectica fibration in the appropriate way, but also to show how Gödel doctrines embody the main logical features of the Dialectica Interpretation. To show that, we derive the soundness of the interpretation of the implication connective, as expounded by Troelstra, in the categorical model. This requires extra logical principles, going beyond intuitionistic logic, namely (suitable versions of) the Markov Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight correspondence between the logical system and the categorical framework. This tight correspondence should come in handy not only when discussing the traditional applications of Dialectica, but also when dealing with some newer uses of the interpretation, as in modelling games or concurrency theory. Finally, to complete our analysis, we characterise categories obtained as a result of the Hyland, Johnstone and Pitts tripos-to-topos construction when applied to Gödel doctrines. [ABSTRACT FROM AUTHOR]

Algorithms for answering XPath queries on Xml streams have been studied intensively in the last decade. Nevertheless, there still exists no solution with high efficiency and large coverage. In this paper, we introduce early nested word automata in order to approximate earliest query answering algorithms for nested word automata. Our early query answering algorithm is based on stack-and-state sharing for running early nested word automata on all answer candidates with on-the-fly determinization. We prove tight upper complexity bounds on time and space consumption. We have implemented our algorithm in the QuiXPath system and show that it outperforms all previous tools in coverage on the XPathMark benchmark, while obtaining very high time and space efficiency and scaling to huge Xml streams. Furthermore, it turns out that our early query answering algorithm is earliest in practice on most queries from the XPathMark benchmark. 1 1 Thanks to the QuiXProc project of Inria and Innovimax and the Cnrs Sosp project. [ABSTRACT FROM AUTHOR]

Although there have been many works on bounded semantics, a characterization of a good definition for a bounded semantics has not been given, and this has led to definitions of bounded semantics of temporal logics that may not be appropriate with respect to the potential usefulness as a basis for developing bounded model checking approaches. On the other side, the research effort on bounded semantics has mainly focused on existentially interpreted fragments of temporal logics, due to the intricacy of defining appropriate bounded semantics for universally interpreted fragments, or for temporal logics with path quantifiers that are closed under negation. This work addresses these two problems, by defining the characteristics of bounded semantics for clarifying the concept of bounded semantics, and presenting a bounded semantics for the full set of CTL, a logic closed under negation, including possibility for specifying both existential and universal properties. [ABSTRACT FROM AUTHOR]

Dynamic graph theory is a novel, growing area that deals with graphs that change over time and is of great utility in modeling modern wireless, mobile and dynamic environments. As a graph evolves, possibly arbitrarily, it is challenging to identify the graph properties that can be preserved over time and understand their respective computability. In this paper we are concerned with the treewidth of dynamic graphs. We focus on metatheorems , which allow the generation of a series of results based on general properties of classes of structures. In graph theory two major metatheorems on treewidth provide complexity classifications by employing structural graph measures and finite model theory. Courcelle's Theorem gives a general tractability result for problems expressible in monadic second order logic on graphs of bounded treewidth, and Frick and Grohe demonstrate a similar result for first order logic and graphs of bounded local treewidth. We extend these theorems by showing that dynamic graphs of bounded (local) treewidth where the length of time over which the graph evolves and is observed is finite and bounded can be modeled in such a way that the (local) treewidth of the underlying graph is maintained. We show the application of these results to problems in dynamic graph theory and dynamic extensions to static problems. In addition we demonstrate that certain widely used dynamic graph classes have bounded local treewidth. [ABSTRACT FROM AUTHOR]

This paper presents a practical decision procedure for Propositional Projection Temporal Logic with infinite models. First, a set Prop l of labels l i , 0 ⩽ i ⩽ n ∈ N 0 , is used to mark nodes of an LNFG of a formula, and a node with l i is treated as an accepting state as in an automaton. Further, the generalized Büchi accepting condition for automata is employed to identify a path (resulting a word) in an LNFG as a model of the formula. In addition, the implementation details of the decision procedure and relevant algorithms including pre-processing, LNFG, circle finding algorithms are presented; as a matter of fact, all algorithms are implemented by C++ programs. [ABSTRACT FROM AUTHOR]

The problem of automated theorem finding is one of the 33 basic research problems in automated reasoning which was originally proposed by Wos in 1988, and it is still an open problem. To solve the problem, an approach of forward deduction based on the strong relevant logics was proposed. Following the approach, this paper presents a systematic methodology for automated theorem finding. To show the effectiveness of our methodology, the paper presents two case studies, one is automated theorem finding in NBG set theory and the other is automated theorem finding in Peano's arithmetic. Some known theorems have been found in our case studies. [ABSTRACT FROM AUTHOR]

Abstract: The aim of this paper is to obtain a theoretical foundation of inconsistency-tolerant (or paraconsistent) reasoning by presenting a comprehensive study of the structural proof-theory of David Nelson’s paraconsistent logic. Inconsistency handling has a growing importance in Computer Science since inconsistencies may frequently occur in knowledge-based and intelligent information systems. Paraconsistent, inconsistency-tolerant logics have been studied to cope with such inconsistencies. In this paper, proof systems for Nelson’s paraconsistent logic N4 are comprehensively studied. The logic N4 is a fundamental system and known to be a common basis for various extended and useful paraconsistent logics. Some basic theorems including cut-elimination, normalization and completeness are uniformly proved using various embedding theorems. A variety of sequent calculi and natural deduction systems for N4 and some closely related systems are presented and compared. [Copyright &y& Elsevier]

Abstract: Inspired by the Multiplicative Exponential fragment of Linear Logic, we define a framework called the prismoid of resources where each vertex is a language which refines the -calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of -reduction, confluence, preservation of -strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter of the formalism, so that all the properties for each vertex are obtained as a particular case of the general abstract proofs. [Copyright &y& Elsevier]

Abstract: A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems. [Copyright &y& Elsevier]

Abstract: In this paper, we consider the robust interpretation of Metric Temporal Logic (MTL) formulas over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with non-trivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we propose multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance, , from unsatisfiability. We prove that any other signal that remains -close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. Finally, our framework is applied to the problem of testing formulas of two fragments of MTL, namely Metric Interval Temporal Logic (MITL) and closed Metric Temporal Logic (clMTL), over continuous-time signals using only discrete-time analysis. The motivating idea behind our approach is that if the continuous-time signal fulfills certain conditions and the discrete-time signal robustly satisfies the temporal logic specification, then the corresponding continuous-time signal should also satisfy the same temporal logic specification. [Copyright &y& Elsevier]

Abstract: Certain behavioral properties of distributed systems are difficult to express in interleaving semantics, whereas they are naturally expressed in terms of partial orders of events or, equivalently, Mazurkiewicz traces. Two examples of such properties are serializability of a database and global snapshots of concurrent systems. Recently, a modest extension for LTL by an operator that expresses snapshots, has been proposed. It combines the ease of linear (interleaving) specification with this useful partial order concept. The new construct allows one to assert that a global snapshot appeared in the past, perhaps not in the observed execution sequence, but possibly in an equivalent one. Originally, a model checking algorithm for this logic that is exponential space in the size of the system was suggested. In this paper, we provide a model checking algorithm that is in polynomial space in the size of the system. Our construction can also serve as an efficient (polynomial) algorithm for detecting conjunctive properties (i.e., conjunction of local process properties) in a concurrent history of execution. [Copyright &y& Elsevier]

Abstract: The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network. [Copyright &y& Elsevier]

Abstract: Commutative, integral and bounded -algebras form a subvariety of residuated lattices which provides the algebraic semantics of an interesting common fragment of intuitionistic logic and of several fuzzy logics. It is known that both the equational theory and the quasiequational theory of commutative -algebras are decidable (in contrast to the noncommutative case), but their complexity has not been studied yet. In this paper, we prove that both theories are in , and that the quasiequational theory is -hard. [Copyright &y& Elsevier]

Abstract: Eilenberg, Elgot and Shepherdson showed in 1969, [S. Eilenberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by -tape automata, Journal of Algebra 13 (1969) 447–464], that a relation on finite words over a finite, non-unary alphabet with letters is definable in first order logic with predicates for the relations equal length, prefix and last letter is (for each letter ) if and only if it can be recognized by a finite multitape synchronous automaton, i.e., one whose read heads move simultaneously. They left open the characterization in the case of infinite alphabets, and proposed some conjectures concerning them. We solve all problems and sharpen the main theorem of [S. Eilenberg, C.C. Elgot, J.C. Shepherdson, Sets recognized by -tape automata, Journal of Algebra 13 (1969) 447–464]. [Copyright &y& Elsevier]

Abstract: This is a survey of results about versions of fine hierarchies and many-one reducibilities that appear in different parts of theoretical computer science. These notions and related techniques play a crucial role in understanding complexity of finite and infinite computations. We try not only to present the corresponding notions and facts from the particular fields but also to identify the unifying notions, techniques and ideas. [Copyright &y& Elsevier]

Abstract: We consider the notion of modular decomposition for countable graphs. The modular decomposition of a graph given with an enumeration of its set of vertices can be defined by formulas of monadic second-order logic. Another result is the definition of a representation of modular decompositions by low degree relational structures. Such relational structures can also be defined in the considered graph by monadic second-order formulas. [Copyright &y& Elsevier]

Abstract: We solve the Angel Problem, by describing a strategy that guarantees the win of an Angel of power 2 or greater. Basically, the Angel should move north as quickly as possible. However, he should detour around eaten squares, as long as the extra distance does not exceed twice the number of eaten squares evaded. We show that an Angel following this strategy will always spot a trap early enough to avoid it. [Copyright &y& Elsevier]

Abstract: We develop possible worlds (Kripke) semantics at the categorical abstract model theoretic level provided by the so-called ‘institutions’. Our general abstract modal logic framework provides a method for systematic Kripke semantics extensions of logical systems from computing science and logic. We also extend the institution-independent method of ultraproducts of [R. Diaconescu, Institution-independent ultraproducts, Fundamenta Informaticæ 55 (3–4) (2003) 321–348] to possible worlds semantics and prove a fundamental preservation result for abstract modal satisfaction. As a consequence we develop a generic compactness result for possible worlds semantics. [Copyright &y& Elsevier]

Abstract: We introduce a complexity measure of modal properties of finite structures which generalises the automaticity of languages. It is based on graph-automata-like devices called labelling systems. We define a measure of the size of a structure that we call rank, and show that any modal property of structures can be approximated up to any fixed rank by a labelling system. The function that takes to the size of the smallest labelling system doing this is called the labelling index of the property. We demonstrate that this is a useful and fine-grained measure of complexity and show that it is especially well suited to characterise the expressive power of modal fixed-point logics. From this we derive several separation results of modal and non-modal fixed-point logics, some of which are already known whereas others are new. [Copyright &y& Elsevier]

Abstract: The typical AI problem is that of making a plan of the actions to be performed by a robot so that the robot could get into a set of final situations, if it started with a certain initial situation. The planning problem is known to be generally very complex. Even within the case of ‘well-balanced’ actions, strong planning under uncertainty about the effects of actions, or games such as ‘Robot against Nature’, is EXPTIME-complete. As a result, AI planners are very sensitive to the number of the variables involved in making a plan, the inherent symmetry of the problem, and the nature of the logical formalisms being used. This paper shows that linear logic provides a convenient and adequate tool for representing strong and weak planning problems in non-deterministic domains. A particular focus of this paper is on planning problems with an unbounded number of functionally identical objects. We show that for such problems linear logic is especially effective and leads to a dramatic contraction of the search space from exponential to polynomial in size. We employ the ability of linear logic to reason about multisets, which in this instance are created by identifying several distinct objects as being functionally equivalent for the problem at hand (think of a number of balls, each of which must be moved to some new location — the balls are distinct, but are functionally equivalent for the problem). In linear logic terms, we establish a clear syntactic condition that allows us to show that solving a generic planning problem where there is only one generic object, directly implies a solution to the original real planning problem over several real objects, the isomorphic copies of the generic object. Moreover, this correspondence also guarantees to produce a real solution that works in polynomial time. [Copyright &y& Elsevier]

Abstract: We show that a class of vertex partitioning problems that can be expressed in monadic second order logic (MSOL) are polynomials on graphs of bounded clique-width. This class includes coloring, -free coloring, domatic number and partition into perfect graphs. Moreover we show that a class of vertex and edge partitioning problems are polynomials on graphs of bounded treewidth. [Copyright &y& Elsevier]

Abstract: For a propositional proof system we introduce the complexity class of all disjoint -pairs for which the disjointness of the pair is efficiently provable in the proof system . We exhibit structural properties of proof systems which make canonical -pairs associated with these proof systems hard or complete for . Moreover, we demonstrate that non-equivalent proof systems can have equivalent canonical pairs and that depending on the properties of the proof systems different scenarios for and the reductions between the canonical pairs exist. [Copyright &y& Elsevier]

Abstract: Context-aware computing refers to a paradigm in which applications sense aspects of the environment and use this information to adjust their behavior in response to changing circumstances. In this paper, we present a formal model and notation (Context UNITY) for expressing quintessential aspects of context-aware computations; existential quantification, for instance, proves to be highly effective in capturing the notion of discovery in open systems. Furthermore, Context UNITY treats context in a manner that is relative to the specific needs of an individual application and promotes an approach to context maintenance that is transparent to the application. In this paper, we construct the model from first principles, introduce its proof logic, and demonstrate how the model can be used as an effective abstraction tool for context-aware applications and middleware. [Copyright &y& Elsevier]

Abstract: In this paper we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs. [Copyright &y& Elsevier]

Abstract: We present a trace semantics for a language of parallel programs which share access to mutable data. We introduce a resource-sensitive logic for partial correctness, based on a recent proposal of O’Hearn, adapting separation logic to the concurrent setting. The logic allows proofs of parallel programs in which “ownership” of critical data, such as the right to access, update or deallocate a pointer, is transferred dynamically between concurrent processes. We prove soundness of the logic, using a novel “local” interpretation of traces which allows accurate reasoning about ownership. We show that every provable program is race-free. [Copyright &y& Elsevier]

Abstract: In this paper, we introduce the split game, a variant of the Ehrenfeucht–Fraïssé game from logic, which is useful for analyzing the expressive power of classes of generalized regular expressions. An extension of the split game to generalized -regular expressions is also established. To gain insight into how the split game can be applied to attack the long-standing generalized star height 2 problem, we propose and solve the omega power problem, a similar but tractable problem in the context of -languages. Namely we show that omega powers, together with boolean combinations and concatenations, are not sufficient to express the class of -regular languages. [Copyright &y& Elsevier]

Abstract: The advent of proof-carrying code has generated significant interest in reasoning about low-level languages. It is widely believed that low-level languages with jumps must be difficult to reason about because of being inherently non-modular. We argue that this is untrue. We take it seriously that, unlike statements of a high-level language, pieces of low-level code are multiple-entry and multiple-exit. And we define a piece of code as consisting of either a single labelled instruction or a finite union of pieces of code. Thus we obtain a compositional natural semantics and a matching Hoare logic for a basic low-level language with jumps. By their simplicity and intuitiveness, these are comparable to the standard natural semantics and Hoare logic of While. The Hoare logic is sound and complete wrt the semantics and allows for compilation of proofs of the Hoare logic of While. [Copyright &y& Elsevier]

Abstract: Rewriting logic is a flexible and expressive logical framework that unifies algebraic denotational semantics and structural operational semantics (SOS) in a novel way, avoiding their respective limitations and allowing succinct semantic definitions. The fact that a rewrite logic theory’s axioms include both equations and rewrite rules provides a useful “abstraction dial” to find the right balance between abstraction and computational observability in semantic definitions. Such semantic definitions are directly executable as interpreters in a rewriting logic language such as Maude, whose generic formal tools can be used to endow those interpreters with powerful program analysis capabilities. [Copyright &y& Elsevier]

Abstract: We show that some simple and useful stutter-invariant properties definable in the language of Lamport''s Simple Temporal Logic of Actions (STLA) are not definable in STLA and present a natural extension of STLA that allows one to express all stutter-invariant properties definable in the language of STLA. [Copyright &y& Elsevier]

Abstract: We develop a general method for proving properties of contract-signing protocols using a specialized protocol logic. The method is applied to the Asokan–Shoup–Waidner and the Garay–Jacobson–MacKenzie protocols. Our method offers certain advantages over previous analysis techniques. First, it is compositional: the security guarantees are proved by combining the independent proofs for the three subprotocols of each protocol. Second, the formal proofs are carried out in a “template” form, which gives us a reusable proof that may be instantiated for the two example protocols, as well as for other protocols with the same arrangement of messages. Third, the proofs follow the design intuition. In particular, in proving game-theoretic properties like fairness, we demonstrate success for the specific strategy that the protocol designer had in mind, instead of non-constructively proving that a strategy exists. Finally, our logical proofs demonstrate security when an unbounded number of sessions are executed in parallel. [Copyright &y& Elsevier]

Abstract: We define a weighted monadic second order logic for trees where the weights are taken from a commutative semiring. We prove that a restricted version of this logic characterizes the class of formal tree series which are accepted by weighted bottom-up finite state tree automata. The restriction on the logic can be dropped if additionally the semiring is locally finite. This generalizes corresponding classical results of Thatcher, Wright, and Doner for tree languages and it extends recent results of Droste and Gastin [Weighted automata and weighted logics, in: Automata, Languages and Programming—32nd International Colloquium, ICALP 2005, Lisbon, Portugal, 2005, Proceedings, Lecture Notes in Computer Science, Vol. 3580, Springer, Berlin, 2005, pp. 513–525, full version in Theoretical Computer Science, to appear.] from formal power series on words to formal tree series. [Copyright &y& Elsevier]

Abstract: In this paper we compare the semantical and syntactical definitions of extensions for open default theories. We prove that, over monadic languages, these definitions are equivalent and do not depend on the cardinality of the underlying infinite world. We also show that, under the domain closure assumption, one free variable open default theories are decidable. [Copyright &y& Elsevier]

Abstract: Rewriting logic (RL) is a logic of actions whose models are concurrent systems. Rewrite theories involve the specification of equational theories of data and state structures together with a set of rewrite rules that model the dynamics of concurrent systems. Since its introduction, more than one decade ago, RL has attracted the interest of both theorists and practitioners, who have contributed in showing its generality as a semantic and logical framework and also as a programming paradigm. The experimentation conducted in these years has suggested that some significant extensions to the original definition of the logic would be very useful in practice. These extensions may develop along several dimensions, like the choice of the underlying equational logic, the kind of side conditions allowed in rewrite rules and operational concerns for the execution of certain rewrites. In particular, the Maude system now supports subsorting and conditional sentences in the equational logic for data, and also frozen arguments to block undesired nested rewrites; moreover, it allows equality and membership assertions in rule conditions. In this paper, we give a detailed presentation of the inference rules, model theory, and completeness of such generalized rewrite theories. Our results provide a mathematical semantics for Maude, and a foundation for formal reasoning about Maude specifications. [Copyright &y& Elsevier]

Abstract: We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of sequent calculus by an appropriate scoping mechanism. The algorithm given by this proof seems to be more practical than that given by the original proof. A naive implementation is given at the end of the paper. Another contribution is to show that this result extends to a large class of theories, including simple type theory (higher-order logic) and second-order propositional logic. We obtain this way a new proof of the decidability of the inhabitation problem for positive types in system F. [Copyright &y& Elsevier]

Abstract: Full first-order linear logic can be presented as an abstract logic programming language in Miller''s system Forum, which yields a sensible operational interpretation in the ‘proof search as computation’ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first-order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system. [Copyright &y& Elsevier]

Abstract: Periodicity constraints are used in many logical formalisms, in fragments of Presburger LTL, in calendar logics, and in logics for access control, to quote a few examples. In the paper, we introduce the logic , an extension of Linear-Time Temporal Logic LTL with past-time operators whose atomic formulae are defined from a first-order constraint language dealing with periodicity. Although the underlying constraint language is a fragment of Presburger arithmetic shown to admit a PSPACE-complete satisfiability problem, we establish that model-checking and satisfiability problems remain in PSPACE as plain LTL (full Presburger LTL is known to be highly undecidable). This is particularly interesting for dealing with periodicity constraints since the language of has a language more concise than existing languages and the temporalization of our first-order language of periodicity constraints has the same worst case complexity as the underlying constraint language. Finally, we show examples of introduction the quantification in the logical language that provide to , EXPSPACE-complete problems. As another application, we establish that the equivalence problem for extended single-string automata, known to express the equality of time granularities, is PSPACE-complete by designing a reduction from QBF and by using our results for . [Copyright &y& Elsevier]

Abstract: An infinitary proof theory is developed for modal logics whose models are coalgebras of polynomial functors on the category of sets. The canonical model method from modal logic is adapted to construct a final coalgebra for any polynomial functor. The states of this final coalgebra are certain “maximal” sets of formulas that have natural syntactic closure properties. The syntax of these logics extends that of previously developed modal languages for polynomial coalgebras by adding formulas that express the “termination” of certain functions induced by transition paths. A completeness theorem is proven for the logic of functors which have the Lindenbaum property that every consistent set of formulas has a maximal extension. This property is shown to hold if the deducibility relation is generated by countably many inference rules. A counter-example to completeness is also given. This is a polynomial functor that is not Lindenbaum: it has an uncountable set of formulas that is deductively consistent but has no maximal extension and is unsatisfiable, even though all of its countable subsets are satisfiable. [Copyright &y& Elsevier]

Abstract: In the present article, we study the expressive power of higher-order logics on finite relational structures or databases. First, we give a characterization of the expressive power of the fragments and , for each and each number of alternations of quantifier blocks j. Then, we get as a corollary the expressive power of for each order . From our results, as well as from the results of R. Hull and J. Su, it turns out that no higher-order logic can be complete. Even if we consider the union of higher-order logics of all natural orders, i.e., , we still do not get a complete logic. So, we define a logic which we call variable order logic (VO) which permits the use of untyped relation variables, i.e., variables of variable order, by allowing quantification over orders. We show that this logic is complete, though even non-recursive queries can be expressed in VO. Then we define a fragment of VO and we prove that it expresses exactly the class of r.e. queries. We finally give a characterization of the class of computable queries through a fragment of VO, which is undecidable. [Copyright &y& Elsevier]

Abstract: We develop a quantifier-free logic for deriving consequences of multialgebraic theories. Multialgebras are used as models for nondeterminism in the context of algebraic specifications. They are many sorted algebras with set-valued operations. Formulae are sequents over atoms allowing one to state set-inclusion or identity of 1-element sets (determinacy). We introduce a sound and weakly complete Rasiowa–Sikorski (R–S) logic for proving multialgebraic tautologies. We then extend this system for proving consequences of specifications based on translation of finite theories into logical formulae. Finally, we show how such a translation may be avoided—introduction of the specific cut rules leads to a sound and strongly complete Gentzen system for proving directly consequences of specifications. Besides giving examples of the general techniques of R–S and the specific cut rules, we improve the earlier logics for multialgebras by providing means to handle empty carriers (as well as empty result-sets) without the use of quantifiers, and to derive consequences of theories without translation into another format and without using general cut. [Copyright &y& Elsevier]

Abstract: Stream X-machines are a form of extended finite state machines that has received extensive study in recent years. A stream X-machine describes a system as a finite set of states, an internal store, called memory, and a finite number of transitions between the states, labelled by function names (the processing functions). One of the great benefits of using a stream X-machine to specify a system is its associated testing method. Under certain design for test conditions, this method produces a test suite that can determine the correctness of the implementation, provided that the processing functions of the stream X-machine specification have been correctly implemented (this can be checked by a separate testing process, using the same method or alternative functional methods). However, the application of the stream X-machine based testing method is often encumbered by the restrictive design for test conditions required. In practical applications, these conditions are achieved by designing extra functionality that will have to be disabled after testing has been completed. This is a time consuming process and can often be a source of error. This paper provides a strong generalisation of the existing method, which requires much laxer design for test conditions; these are naturally satisfied in practical applications and, furthermore, can be introduced into any stream X-machine specification without the need to add extra functionality. Consequently, the generalised method can be applied to virtually any system that can be specified by a stream X-machine. [Copyright &y& Elsevier]

Abstract: We consider model checking of timed temporal formulae in durational transition graphs (DTGs), i.e., Kripke structures where transitions have integer durations. Two semantics for DTGs are presented and motivated. We consider timed versions of where subscripts put quantitative constraints on the time it takes before a property is satisfied. We exhibit an important gap between logics where subscripts of the form “” (exact duration) are allowed, and simpler logics that only allow subscripts of the form “” or “” (bounded duration). Without exact durations, model checking can be done in polynomial time, but with exact durations, it becomes -complete or -complete depending on the considered semantics. [Copyright &y& Elsevier]

Abstract: This paper aims at applying the 1 [1] Computation Tree Logic. model checking method to the time Petri net (TPN) model. We show here how to contract its generally infinite state space into a graph that captures all its properties. This graph, called atomic state class graph (ASCG), is finite if and only if, the model is bounded. 2 [2] The number of its reachable markings is finite. Our approach is based on a partition refinement technique, similarly to what is proposed in [Berthomieu, Vernadat, State class constructions for branching analysis of time Petri nets, Lecture Notes in Computer Science, vol. 2619, 2003; Yoneda, Ryuba, CTL model checking of time Petri nets using geometric regions, IEICE Trans. Inf. Syst. E99-D(3) (1998)]. In such a technique, an intermediate abstraction (contraction) of the TPN state space is first built, then refined until properties are restored. Our approach improves the construction of the ASCG in two ways. The first way deals with speeding up the refinement process by using a much more compact intermediate contraction of the TPN state space than those used in [Berthomieu, Vernadat, State class constructions for branching analysis of time Petri nets, Lecture Notes in Computer Science, vol. 2619, 2003; Yoneda, Ryuba, CTL model checking of time Petri nets using geometric regions, IEICE Trans. Inf. Syst. E99-D(3) (1998)]. The second way deals with computing each ASCG node in instead of , being the number of transitions enabled at the node. Experimental results have shown that our improvements have a good impact on performances. [Copyright &y& Elsevier]

Abstract: We define the spatio-temporal logic MTLA as an extension of Lamport''s Temporal Logic of Actions TLA for the specification, verification, and formal development of systems that rely on mobile code. The formalism is validated by an encoding of models written in the mobile UML notation. We identify refinement principles for mobile systems and justify refinements of mobile UML state machines with the help of the MTLA semantics. [Copyright &y& Elsevier]

Abstract: In UML 2.0 sequence diagrams have been considerably extended but their expressiveness and semantics remains problematic in several ways. In other work we have shown how sequence diagrams combined with an OCL liveness template gives us a much richer language for inter-object behaviour specification. In this paper, we give a semantics of these enriched diagrams using labelled event structures. Further, we show how sequence diagrams can be embedded into a true-concurrent two-level logic interpreted over labelled event structures. The top level logic, called communication logic, is used to describe inter-object specification, whereas the lower level logic, called home logic, describes intra-object behaviour. An interesting consequence of using this logic relates to how state-based behaviour can be synthesised from inter-object specifications. Plans of extending the Edinburgh Concurrency Workbench in this context are discussed. [Copyright &y& Elsevier]

Abstract: We are interested in separation-logic-based static analysis of programs that use shared mutable data structures. In this paper, we introduce backward and forward analysis for a separation logic called , an extension of separation logic [Ishtiaq and O’Hearn, BI as an assertion language for mutable data structures, in: POPL’01, 2001, pp. 14–26], to which we add fixpoint connectives and postponed substitution. This allows us to express recursive definitions within the logic as well as the axiomatic semantics of while statements. [Copyright &y& Elsevier]

Abstract: Monadic least fixed point logic MLFP is a natural logic whose expressiveness lies between that of first-order logic FO and monadic second-order logic MSO. In this paper, we take a closer look at the expressive power of MLFP. Our results are: [(1)] MLFP can describe graph properties beyond any fixed level of the monadic second-order quantifier alternation hierarchy. [(2)] On strings with built-in addition, MLFP can describe at least all languages that belong to the linear time complexity class DLIN. [(3)] Settling the question whether or, equivalently, settling the question whether would solve open problems in complexity theory: “” would imply that whereas “” would imply that . Apart from this we give a self-contained proof of the previously known result that MLFP is strictly less expressive than MSO on the class of finite graphs. [Copyright &y& Elsevier]

Abstract: We consider the multiplicative and exponential fragment of linear logic (MELL) and give a geometry of interaction (GoI) semantics for it based on unique decomposition categories. We prove a soundness and finiteness theorem for this interpretation. We show that Girard''s original approach to GoI 1 via operator algebras is exactly captured in this categorical framework. [Copyright &y& Elsevier]

Abstract: Ludics [J.-Y. Girard, Locus solum, Math. Structures in Comput. Sci. 11 (2001) 301–506] is a recent proposal of analysis of interaction, developed by abstracting away from proof-theory. It provides an elegant, abstract setting in which interaction between agents (proofs/programs/processes) can be studied at a foundational level, together with a notion of equivalence from the point of view of the observer. An agent should be seen as some kind of black box. An interactive observation on an agent is obtained by testing it against other agents. In this paper we explore what can be observed interactively in this setting. In particular, we characterize the objects that can be observed in a single test: the primitive observables of the theory. Our approach builds on an analysis of the geometrical properties of the agents, and highlights a deep interleaving between two partial orders underlying the combinatorial structures: the spatial one and the temporal one. [Copyright &y& Elsevier]

Abstract: We define a new class of games, called backtracking games. Backtracking games are essentially parity games with an additional rule allowing players, under certain conditions, to return to an earlier position in the play and revise a choice or to force a countback of the number of moves. This new feature makes backtracking games more powerful than parity games. As a consequence, winning strategies become more complex objects and computationally harder. The corresponding increase in expressiveness allows us to use backtracking games as model-checking games for inflationary fixed-point logics such as IFP or MIC. We identify a natural subclass of backtracking games, the simple games, and show that these are the “right” model-checking games for IFP by (a) giving a translation of formulae and structures into simple games such that if, and only if, Player 0 wins the corresponding game and (b) showing that the winner of simple backtracking games can again be defined in IFP. [Copyright &y& Elsevier]