A Temporal Logic for Proving Properties of Topologically General Executions

We present a generalization of the temporal propositional logic of linear time which is useful for stating and proving properties of the generic execution sequence of a parallel program or a non-deterministic program. The formal system we present is exactly that same as the third of three logics presented by Lehmann and Shelah (Information and Control53, 165–198 (1982)), but we give it a different semantics. The models are tree models of arbitrary size similar to those used in branching time temporal logic. The formulation we use allows us to state properties of the “co-meagre” family of paths, where the term “co-meagre” refers to a set whose complement is of the first category in Baire's classification looking at the set of paths in the model as a metric space. Our system is decidable, sound, and, complete for models of arbitrary size, but it has the finite model property; namely, every sentence having a model has a finite model.     

An Until Hierarchy and Other Applications of an Ehrenfeucht–Fraïssé Game for Temporal Logic

We prove there is a strict hierarchy of expressive power according to the Until depth of linear temporal logic (LTL) formulas: for each k, there is a natural property, based on quantitative fairness, that is not expressible with k nestings of Until operators, regardless of the number of applications of other operators, but is expressible by a formula with Until depth k+1. Our proof uses a new Ehrenfeucht–Fraïssé (EF) game designed specifically for LTL. These properties can all be expressed in first-order logic with quantifier depth and size (log k), and we use them to observe some interesting relationships between LTL and first-order expressibility. We note that our Until hierarchy proof for LTL carries over to the branching time logics, CTL and CTL*. We then use the EF game in a novel way to effectively characterize (1) the LTL properties expressible without Until, as well as (2) those expressible without both Until and Next. By playing the game “on finite automata,” we prove that the automata recognizing languages expressible in each of the two fragments have distinctive structural properties. The characterization for the first fragment was originally proved by Cohen, Perrin, and Pin using sophisticated semigroup-theoretic techniques. They asked whether such a characterization exists for the second fragment. The technique we develop is general and can potentially be applied in other contexts.     

Relativizations for the Logic-Automata Connection

BDDs and their algorithms implement a decision procedure for Quantified Propositional Logic. BDDs are a kind of acyclic automata. But unrestricted automata (recognizing unbounded strings of bit vectors) can be used to decide monadic second-order logics, which are more expressive. Prime examples are WS1S, a number-theoretic logic, or the string-based logical notation of introductory texts. One problem is that it is not clear which one is to be preferred in practice. For example, it is not known whether these two logics are computationally equivalent to within a linear factor, that is, whether a formula ϕ of one logic can be transformed to a formula %phis;′ of the other such that %phis;′ is true if and only if ϕ is and such that ϕ′ is decided in time linear in that of the time for ϕ.Another problem is that first-order variables in either version are given automata-theoretic semantics according to relativizations, which are syntactic means of restricting the domain of quantification of a variable. Such relativizations lead to technical arbitrations that may involve normalizing each subformula in an asymmetric manner or may introduce spurious state space explosions.In this paper, we investigate these problems through studies of congruences on strings. This algebraic framework is adapted to language-theoretic relativizations, where regular languages are intersected with restrictions. The restrictions are also regular languages. We introduce ternary and sexpartite characterizations of relativized regular languages. From properties of the resulting congruences, we are able to carry out detailed state space analyses that allow us to address the two problems.We report briefly on practical experiments that support our results. We conclude that WS1S with first-order variables can be robustly implemented in a way that efficiently subsumes string-based notations.Dedicated to the memory of Bob Paige and his contributions to automata algorithmsSome of the material in this paper appeared in Computer Aided Verification, CAV ‘99, LNCS 1633, 1999, under the title “A theory of restrictions for logics and automata.” This work was carried out while the author was with AT&T Labs–Research; itwas also supported in part by grant CCR-0341658 from the National Science Foundation.     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

Some Logical and Automata-Theoretic Aspects of Product Behaviours

A network of sequential processes that communicate by synchronizing on common actions enjoys the status of a “folklore” model of distributed systems. Despite (because of?) this familiarity it is only recently there has been a systematic study of this model that we call product systems.In particular, it turns out that the classical theory involving Buechi automata, w-regular languages, monadic second order logics and linear time temporal logics extends smoothly to the setting of product systems. We shall survey this theory with an eye towards partial order based temporal logics.     

Logics and Multi-agents: towards a new symbolic model of cognition

The last edition of CLIMA, held in 2001 in Paphos (Cyprus) ended with a panel session on the role of Computational Logic (CL) in Multi-Agent Systems (MAS).Two dimensions in MAS development were singled out and discussed: on the one hand reactivity vs. rationality, and on the other hand individuals vs. societies. Most of the points discussed aimed at justifying and motivating the application of CL techniques to MAS development: should be logics used to implement the individuals, or the society, or both? should be logics used to model the reactive part, or the pro-active part, or both? what do we want to achieve in terms of properties, openness to integration, etc.?A most intuitive reply to these questions could be that logic should be used for what logic is good at. For instance, logic programming-based techniques such as abductive and inductive logic programming seem suitable for modelling agent hypothetical reasoning and adaptability. Modal logic operators such as those adopted by a BDI agent model [3] could be a powerful and synthetic way to describe the agent behaviour and to put it into relationship with the other agents in a society. Model checking-based techniques can be applied to the verification of agent systems. A combination of multiple approaches, like modal and temporal logics, or abduction and induction in a logic programming framework, could be the key to achieve a more comprehensive agent and agent system architecture. But in this case, to determine which properties of the chosen combinations hold is not an easy task.At the time of this new edition of CLIMA, while the debate about the role of CL in MAS is still open, from within the CL community we are witnessing a growth of interest for Multi-Agent Systems considered per se as an interesting cognitive model. This is due to many reasons, among which, we would say, the need to put “abstract” reasoning in the context of a “concrete” environment, and to use logic not only to solve problems in a virtual world, but in a real arena. The multi-agent metaphor of intelligent individuals that are situated into dynamic and unpredictable environments and that can interact with each other by updating their beliefs, can be regarded then as the basis for a new symbolic model of cognition.     

Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

A Practical Approach to Partial Functions in CVC Lite

Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is “the right” logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the “undefined” value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.     

A modal proof theory for final polynomial coalgebras

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.     

Maximal traces and path-based coalgebraic temporal logics

This paper gives a general coalgebraic account of temporal logics whose semantics involves a notion of computation path. Examples of such logics include the logic CTL* for transition systems and the logic PCTL for probabilistic transition systems. Our path-based temporal logics are interpreted over coalgebras of endofunctors obtained as the composition of a computation type (e.g. non-deterministic or stochastic) with a general transition type. The semantics of such logics relies on the existence of execution maps similar to the trace maps introduced by Jacobs and co-authors as part of the coalgebraic theory of finite traces (Hasuo et al., 2007 [1]). We consider finite execution maps derived from the theory of finite traces, and a new notion of maximal execution map that accounts for maximal, possibly infinite executions. The latter is needed to recover the logics CTL* and PCTL as specific path-based logics.     

Efficient Specialisation in Prolog Using the Hand-Written Compiler Generator LOGEN

The so called “cogen approach” to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and imperative languages. In earlier work we have shown that this approach is also applicable to partial evaluation of logic programming languages, also called partial deduction.In this paper we extend upon this by allowing partially instantiated datastructures (via binding types), which are especially important in the context of logic programming. We also extend cogen to directly support a large part of Prolog's declarative and non-declarative features and how semi-online specialisation can be efficiently integrated. Benchmarks show that the resulting cogen is very efficient, generates very efficient generating extensions (executing up to several orders of magnitude faster than current online systems) which in turn perform very good and non-trivial specialisation, even rivalling existing online systems.     

Using Assumptions to Distribute CTL Model Checking

In this work we discuss the problem of performing distributed CTL model checking by splitting the given state space into several “partial state spaces” . The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about the truth of formulas and the computers exchange assumptions about relevant states as they compute more precise information. In the paper we give the basic definitions and present the distributed algorithm.     

A Branching Time Temporal Framework for Quantitative Reasoning

Temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) have become popular for specifying temporal properties over a wide variety of planning and verification problems. In this paper we work towards building a generalized framework for automated reasoning based on temporal logics. We present a powerful extension of CTL with first-order quantification over the set of reachable states for reasoning about extremal properties of weighted labeled transition systems in general. The proposed logic, which we call Weighted Quantified Computation Tree Logic (WQCTL), captures the essential elements common to the domain of planning and verification problems and can thereby be used as an effective specification language in both domains. We show that in spite of the rich, expressive power of the logic, we are able to evaluate WQCTL formulas in time polynomial in the size of the state space times the length of the formula. Wepresent experimental results on the WQCTL verifier.     

Translating Java for Multiple Model Checkers: The Bandera Back-End

One approach to model checking program source code is to view a model checker as a target machine. In this setting, program source code is translated to a model checker’s input language using a process that shares much in common with program compilation. For example, well-defined intermediate program representations are used to stage the translation through a series of analyses and optimizing transformations and target-specific details are isolated in code generation modules.In this paper, we present the Bandera Intermediate Representation (BIR)—a guarded-assignment transformation system language that has been designed to support the translation of Java programs to a variety of model checkers. BIR includes constructs, such as inheritance, dynamic creation of data, and locking primitives, that are designed to model the semantics of Java primitives. BIR also includes several non-deterministic choice constructs that support abstraction in modeling and specification of properties of dynamic heap structures.We have developed a BIR-based tool infrastructure that has been applied to develop customized analysis frameworks for several different input languages using different model checking tools. We present BIR’s type system and operational semantics in sufficient detail to support similar applications by other researchers. This semantics details several state space reductions and state space search variations. We describe the translation of Java to BIR and how BIR is translated to the input languages of several model checkers.     

Branching-time logics with path relativisation

We define extensions of the full branching-time temporal logic CTL^? in which the path quantifiers are relativised by formal languages of infinite words, and consider its natural fragments obtained by extending the logics CTL and CTL⁺ in the same way. This yields a small and two-dimensional hierarchy of temporal logics parametrised by the class of languages used for the path restriction on one hand, and the use of temporal operators on the other. We motivate the study of such logics through two application scenarios: in abstraction and refinement they offer more precise means for the exclusion of spurious traces; and they may be useful in software synthesis where decidable logics without the finite model property are required. We study the relative expressive power of these logics as well as the complexities of their satisfiability and model-checking problems.     

Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes

In a recent paper Baier et al. [Lecture Notes in Computer Science, Springer-Verlag, 2000, p. 358] analyzed a new way of model-checking formulas of a logic for continuous-time processes—called continuous stochastic logic (henceforth CSL)—against continuous-time Markov chains—henceforth CTMCs. One of the important results of that paper was the proof that if two CTMCs were bisimilar then they would satisfy exactly the same formulas of CSL. This raises the converse question—does satisfaction of the same collection of CSL formulas imply bisimilarity? In other words, given two CTMCs which are known to satisfy exactly the same formulas of CSL does it have to be the case that they are bisimilar? We prove that the answer to the question just raised is “yes”. In fact we prove a significant extension, namely that a subset of CSL suffices even for systems where the state space may be a continuum. Along the way we prove a result to the effect that the set of Zeno paths has measure zero provided that the transition rates are bounded.     

Modelling uncertain positive and negative reasons in decision aiding

The use of positive and negative reasons in inference and decision aiding is a recurrent issue of investigation as far as the type of formal language to use within a DSS is concerned. A language enabling to explicitly take into account such reasons is Belnap's logic and the four valued logics derived from it. In this paper, we explore the interpretation of a continuous extension of a four valued logic as a necessity degree (in possibility theory). It turns out that, in order to take full advantage of the four values, we have to consider “sub-normalised” necessity measures. Under such a hypothesis four valued logics become the natural logical frame for such an approach.     

Probabilistic Logic over Paths

We introduce a probabilistic modal logic PPL extending the work of [Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1,2):78–128, 1990; Ronald Fagin and Joseph Y. Halpern. Reasoning about knowledge and probability. Journal of the ACM, 41(2):340–367, 1994] by allowing arbitrary nesting of a path probabilistic operator and we prove its completeness. We prove that our logic is strictly more expressive than other logics such as the logics cited above. By considering a probabilistic extension of CTL we show that this additional expressive power is really needed in some applications.     

Validating for Liveness in Hidden Adversary Systems

Multi-stream interactive systems can be seen as “hidden adversary” systems (HAS), where the observable behaviour on any interaction channel is affected by interactions happening on other channels. One way of modelling HAS is in the form of a multi-process I/O automata, where each interacting process appears as a token in a shared state space. Constraints in the state space specify how the dynamics of one process affects other processes. We define the “liveness criterion” of each process as the end objective to be achieved by the process. The problem now for each process is to achieve this objective in the face of unforeseen interferences from other processes. In an earlier paper, it was proposed that this uncertainty can be mitigated by collaboration among the disparate processes. Two types of collaboration philosophies were also suggested: altruistic collaboration and pragmatic collaboration. This paper addresses the HAS validation problem where processes collaborate altruistically.     

Reductions among number theoretic problems

Many number theoretic problems such as integer factorization and the discrete logarithm problem have defied all attempts to classify their complexities. Thirteen such problems are considered, none of which is known either to have a deterministic polynomial time solution, or to be complete for any natural complexity class. Failing this, the next best goal is to determine which among these are the “easiest” and which are the “hardest” problems. Toward this end, this paper gives an overview of reductions among the problems. Two reductions are new: a deterministic polynomial time reduction from squarefreeness to Euler's function φ(n), and a probabilistic polynomial time reduction from order modulo a prime power to discrete logarithm modulo a prime power.