Future temporal logic needs infinitely many modalities

Kamp’s theorem states that there is a temporal logic with two modalities (“until” and “since”) which is expressively complete for the first-order monadic logic of order over the real line. In this paper we show that there is no temporal logic with finitely many modalities which is expressively complete for the future fragment of first-order monadic logic of order over the real line (a future formula over the real time line is a formula whose truth value at a point is independent of what happened in the past).     

First-Order Logic with Two Variables and Unary Temporal Logic

We investigate the power of first-order logic with only two variables over ω-words and finite words, a logic denoted by FO². We prove that FO² can express precisely the same properties as linear temporal logic with only the unary temporal operators: “next,” “previously,” “sometime in the future,” and “sometime in the past,” a logic we denote by unary-TL Moreover, our translation from FO² to unary-TL converts every FO² formula to an equivalent unary-TL formula that is at most exponentially larger and whose operator depth is at most twice the quantifier depth of the first-order formula. We show that this translation is essentially optimal. While satisfiability for full linear temporal logic, as well as for unary-TL, is known to be PSPACE-complete, we prove that satisfiability for FO² is NEXP-complete, in sharp contrast to the fact that satisfiability for FO³ has nonelementary computational complexity. Our NEXP upper bound for FO² satisfiability has the advantage of being in terms of the quantifier depth of the input formula. It is obtained using a small model property for FO² of independent interest, namely, a satisfiable FO² formula has a model whose size is at most exponential in the quantifier depth of the formula. Using our translation from FO² to unary-TL we derive this small model property from a corresponding small model property for unary-TL. Our proof of the small model property for unary-TL is based on an analysis of unary-TL types.     

Expressing Priorities and External Probabilities in Process Algebra via Mixed Open/Closed Systems

Defining operational semantics for a process algebra is often based either on labeled transition systems that account for interaction with a context or on the so-called reduction semantics: we assume to have a representation of the whole system and we compute unlabeled reduction transitions (leading to a distribution over states in the probabilistic case). In this paper we consider mixed models with states where the system is still open (towards interaction with a context) and states where the system is already closed. The idea is that (open) parts of a system “P” can be closed via an operator “P↑G” that turns already synchronized actions whose “handle” is specified inside “G” into prioritized reduction transitions (and, therefore, states performing them into closed states). We show that we can use the operator “P↑G” to express multi-level priorities and external probabilistic choices (by assigning weights to handles inside G), and that, by considering reduction transitions as the only unobservable τ transitions, the proposed technique is compatible, for process algebra with general recursion, with both standard (probabilistic) observational congruence and a notion of equivalence which aggregates reduction transitions in a (much more aggregating) trace based manner. We also observe that the trace-based aggregated transition system can be obtained directly in operational semantics and we present the “aggregating” semantics. Finally, we discuss how the open/closed approach can be used to also express discrete and continuous (exponential probabilistic) time and we show that, in such timed contexts, the trace-based equivalence can aggregate more with respect to traditional lumping based equivalences over Markov Chains.     

Adding For-Loops to First-Order Logic

We study the query language BQL: the extension of the relational algebra with for-loops. We also study FO(FOR): the extension of first-order logic with a for-loop variant of the partial fixpoint operator. In contrast to the known situation with query languages, which include while-loops instead of for-loops, BQL and FO(FOR) are not equivalent. Among the topics we investigate are: the precise relationship between BQL and FO(FOR); inflationary versus noninflationary iteration; the relationship with logics that have the ability to count; and nested versus unnested loops.     

A Partial Order Approach to Branching Time Logic Model Checking

Partial order techniques enable reducing the size of the state space used for model checking, thus alleviating the “state space explosion” problem. These reductions are based on selecting a subset of the enabled operations from each program state. So far, these methods have been studied, implemented, and demonstrated for assertional languages that model the executions of a program as computation sequences, in particular the linear temporal logic. The present paper shows, for the first time, how this approach can be applied to languages that model the behavior of a program as a tree. We study here partial order reductions for branching temporal logics, e.g., the logics CTL and CTL* (with the next time operator removed) and process algebra logics such as Hennesy–Milner logic (withτactions). Conditions on the selection of subset of successors from each state during the state-space construction, which guarantee reduction that preserves CTL* properties, are given. The experimental results provided show that the reduction is substantial.     

On the complemented disk algebra

The importance of relational methods in temporal and spatial reasoning has been widely recognised in the last two decades. A quite large part of contemporary spatial reasoning is concerned with the research of relation algebras generated by the “part of” and “connection” relations in various domains. This paper is devoted to the study of one particular relation algebra appeared in the literature, viz. the complemented disk algebra. This algebra was first described by Düntsch [I. Düntsch, A tutorial on relation algebras and their application in spatial reasoning, Given at COSIT, August 1999, Available from: <http://www.cosc.brocku.ca/~duentsch/papers/relspat.html>] and then, Li et al. [Y. Li, S. Li, M. Ying, Relational reasoning in the Region Connection Calculus, Preprint, 2003, Available from: http://arxiv.org/abs/cs/0505041] showed that closed disks and their complements provides a representation. This set of regions is rather restrictive and, thus, of limited practical values. This paper will provide a general method for generating representations of this algebra in the framework of Region Connection Calculus. In particular, connected regions bounded by Jordan curves and their complements is also such a representation.     

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF

Software that can produce independently checkable evidence for the correctness of its output has received recent attention for use in certifying compilers and proof-carrying code. CVC (Cooperating Validity Checker) is a proof-producing validity checker for a decidable fragment of first-order logic enriched with background theories. This paper describes how proofs of valid formulas are produced from the decision procedure for linear real arithmetic implemented in CVC. It is shown how extensions to LF which support proof rules schematic in an arity (“elliptical” rules) are very convenient for this purpose.     

The μ-calculus as an assertion-language for fairness arguments

Various principles of proof have been proposed to reason about fairness. This paper addresses—for the first time—the question in what formalism such fairness arguments can be couched. To wit: we prove that Park's monotone first-order μ-calculus, augmented with constants for all recursive ordinals can serve as an assertion-language for proving fair termination of do-loops. In particular, the weakest precondition for fair termination of a loop w.r.t. some postcondition is definable in it. The relevance of this result to proving eventualities in the temporal logic formalism of Manna and Pnuelis (in “Foundations of Computer Science IV, Part 2,” Math. Centre Tracts, Vol. 159, Math. Centrum, Amsterdam, 1983) is discussed.     

On the absence of strict boundaries—Vagueness, haziness, and fuzziness in philosophy, science, and medicine

This contribution deals with developments in the history of philosophy, logic, and mathematics during the time before and up to the beginning of fuzzy logic. Even though the term “fuzzy” was introduced by Lotfi A. Zadeh in 1964/1965, it should be noted that older concepts of “vagueness” and “haziness” had previously been discussed in philosophy, logic, mathematics, applied sciences, and medicine. This paper delineates some specific paths through the history of the use of these “loose concepts”. Vagueness was avidly discussed in the fields of logic and philosophy during the first decades of the 20th century—particularly in Vienna, at Cambridge and in Warsaw and Lvov. An interesting sequel to these developments can be seen in the work of the Polish physician and medical philosopher Ludwik Fleck.Haziness and fuzziness were concepts of interest in mathematics and engineering during the second half of the 1900s. The logico-philosophical history presented here covers the work of Bertrand Russell, Max Black, and others. The mathematical–technical history deals with the theories founded by Karl Menger and Lotfi Zadeh. Menger's concepts of probabilistic metrics, hazy sets (ensembles flous) and micro-geometry as well as Zadeh's theory of fuzzy sets paved the way for the establishment of soft computing methods using vague concepts that connote the nonexistence of sharp boundaries.     

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.     

Languages Defined with Modular Counting Quantifiers

We prove that a regular language defined by a boolean combination of generalized Σ₁-sentences built using modular counting quantifiers can be defined by a boolean combination of Σ₁-sentences in which only regular numerical predicates appear. The same statement, with “Σ₁” replaced by “first-order,” is equivalent to the conjecture that the nonuniform circuit complexity class ACC is strictly contained in NC¹. The argument introduces some new techniques, based on a combination of semigroup theory and Ramsey theory, which may shed some light on the general case.     

Countering the loss of extended vigilance in supervisory control using a fuzzy logic model

When an operator first detects unusual and/or infrequent or irregular signals in a system, the operator does not need to take any action, but must increase his/her level of attention and be alert for any more serious signals that may confirm a problem with the system. This is referred to as extended vigilance. The purpose of this study was to construct a fuzzy vigilance-measuring model for countering the loss of extended vigilance. The model extends two-valued logic (“Yes” or “No”) to multi-valued logic through fuzzy sets. Then a fuzzy logic alarm was developed by the model for combating the extended vigilance decrement. The first experiment compared the effect of the fuzzy measuring model with signal detection theory (SDT) and discussed the relationship between preliminary and extended vigilance for a simulated feed-water monitoring system. The results indicated that the sensitivity of the fuzzy vigilance-measuring model is better than index d′ and β, and that the preliminary vigilance significantly influences the extended vigilance. The second experiment verified the effect of the fuzzy logic alarm. The results indicated that the effect of the fuzzy logic alarm for combating the extended vigilance decrement is significant. When the preliminary vigilance is poor, an appropriate alarm will improve the extended vigilance. However, if the preliminary vigilance is very poor, the improvement of the extended vigilance will be limited.Relevance to industry: The extended vigilance is a new and important issue in human performance problems in industry, particularly in such areas as air-traffic control, industrial inspection and power plant monitor. The measuring model of vigilance could be applied to develop an alarm for promoting supervisory performance of human and human–machine detectors.     

An Integrated Approach for the Specification and Analysis of Stochastic Real-Time Systems

The usage of process algebras for the performance modeling and evaluation of concurrent systems turned out to be convenient due to their feature of compositionality. A particularly simple and elegant solution in this field is the calculus of Interactive Markov Chains (IMCs), where the behavior of processes is just represented by Continuous Time Markov Chains extended with action transitions representing process interaction. The main advantage of IMCs with respect to other existing approaches is that a notion of bisimulation which abstracts from τ-transitions (“complete” interactions) can be defined which is a congruence. However in the original definition of the calculus of IMCs the high potentiality of compositionally minimizing the system state space given by the usage of a “weak” notion of equivalence and the elegance of the approach is somehow limited by the fact that the equivalence adopted over action transitions is a finer variant of Milner's observational congruence that distinguishes τ-divergent “Zeno” processes from non-divergent ones. In this paper we show that it is possible to reformulate the calculus of IMCs in such a way that we can just rely on simple standard observational congruence. Moreover we show that the new calculus is the first Markovian process algebra allowing for a new notion of Markovian bisimulation equivalence which is coarser than the standard one.     

Database Query Processing Using Finite Cursor Machines

We introduce a new abstract model of database query processing, finite cursor machines, that incorporates certain data streaming aspects. The model describes quite faithfully what happens in so-called “one-pass” and “two-pass query processing”. Technically, the model is described in the framework of abstract state machines. Our main results are upper and lower bounds for processing relational algebra queries in this model, specifically, queries of the semijoin fragment of the relational algebra.     

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.     

Infinitary Logic and Inductive Definability over Finite Structures

The extensions of first-order logic with a least fixed point operator (FO + LFP) and with a partial fixed point operator (FO + PFP) are known to capture the complexity classes P and PSPACE respectively in the presence of an ordering relation over finite structures. Recently, Abiteboul and Vianu (in "Proceedings of the 23rd ACM Symposium on the Theory of Computing," 1991) investigated the relationship of these two logics in the absence of an ordering, using a machine model of generic computation. In particular, they showed that the two languages have equivalent expressive power if and only if P = PSPACE. These languages can also be seen as fragments of an infinitary logic where each formula has a bounded number of variables, L^ω_∞ω, (see, for instance, Kolaitis and Vardi, in "Proceedings of the 5th IEEE Symposium on Logic in Computer Science," pp. 156-167, 1990). We investigate this logic on finite structures and provide a normal form for it. We also present a treatment of Abiteboul and Vianu′s results from this point of view. In particular, we show that we can write a formula of FO + LFP that defines an ordering of the L^k_∞ω, types uniformly over all finite structures. One consequence of this is a generalization of the equivalence of FO + LFP and P from ordered structures to classes of structures where every element is definable. We also settle a conjecture mentioned by Abiteboul and Vianu by showing that FO + LFP is properly contained in the polynomial time computable fragment of L^ω_∞ω, raising the question of whether the latter fragment is a recursively enumerable class.     

Stability and performance analysis of mixed product run-to-run control

Run-to-run control has been widely used in batch manufacturing processes to reduce variations. However, in batch processes, many different products are fabricated on the same set of process tool with different recipes. Two intuitive ways of defining a control scheme for such a mixed production mode are (i) each run of different products is used to estimate a common tool disturbance parameter, i.e., a “tool-based” approach, (ii) only a single disturbance parameter that describe the combined effect of both tool and product is estimated by results of runs of a particular product on a specific tool, i.e., a “product-based” approach. In this study, a model two-product plant was developed to investigate the “tool-based” and “product-based” approaches. The closed-loop responses are derived analytically and control performances are evaluated. We found that a “tool-based” approach is unstable when the plant is non-stationary and the plant-model mismatches are different for different products. A “product-based” control is stable but its performance will be inferior to single product control when the drift is significant. While the controller for frequent products can be tuned in a similar manner as in single product control, a more active controller should be used for the infrequent products which experience a larger drift between runs. The results were substantiated for a larger system with multiple products, multiple plants and random production schedule.     

Relational theory of queries

In this paper a new presentation of the relational theory of queries will be given. Both the relational algebra and the (domain) relational calculus will be systematically derived from first-order logic. The connections between logic, algebra and calculus will become extremely simple: e.g. the relational algebra will be isomorphic with a subset of relational calculus. Also some theoretical results about the completeness of the relational query languages will be presented. Both the relational calculus and the relational algebra will be extended to contain aggregate functions.     

On the computation of the gap metric for LTV systems

In this paper, we consider the robust stabilization problem for linear discrete time-varying (LTV) systems using the gap metric. In particular, we show that the time-varying (TV) directed gap reduces to an operator with a TV Hankel plus Toeplitz structure. Computation of the norm of such an operator can be carried out using an iterative scheme involving a TV Hankel operator defined on a space of Hilbert–Schmidt causal operators. The “infimization” in the TV directed gap formula is shown to be, in fact, a minimum by using duality theory. The latter holds as well in the time-invariant case.     

Generic Trace Theory

Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism” such as classical non-determinism (with a set of possible choices) vs. probabilistic non-determinism. In this paper we claim that these various forms of “trace semantics” are instances of a single categorical construction, namely coinduction in a Kleisli category. This claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in the work of Smyth and Plotkin.