The monadic second-order logic of graphs,II: Infinite graphs of bounded width

A countable graph can be considered as the value of a certain infinite expression, represented itself by an infinite tree. We establish that the set of finite or infinite (expression) trees constructed with a finite number of operators, the value of which is a graph satisfying a property expressed in monadic second-order logic, is itself definable in monadic second-order logic. From Rabin's theorem, the emptiness of this set of (expression) trees is decidable. It follows that the monadic second-order theory of an equational graph, or of the set of countable graphs of width less than an integerm, is decidable. This work has been supported by the “Programme de Recherches Coordonnées: Mathématiques et Informatique.” Reprints can be requested by electronic mail at mcvax!inria!geocub!courcell (on UUCP network) or courcell@geocub.greco-prog.fr. Unité de Recherche associée au C.N.R.S. no. 726.     

The monadic second-order logic of graphs IX: Machines and their behaviours

We establish that every monadic second-order property of the behaviour of a machine (transition systems and tree automata are typical examples of machines) is a monadic second-order property of the machine itself. In this way, we clarify the distinction between “dynamic” properties of machines (i.e., properties of their behaviours), and their “static” properties (i.e., properties of the graphs or relational structures representing them). It is important for program verification that the dynamic properties that one wants to verify can be formulated statically, in the simplest possible way. As a corollary of our main result, we also obtain that the monadic theory of an algebraic tree is decidable.     

The monadic second-order logic of graphs V: on closing the gap between definability and recognizability

Context-free graph-grammars are considered such that, in every generated graph G, a derivation tree of G can be constructed by means of monadic second-order formulas that specify its nodes, its labels, the successors of a node etc. A subset of the set of graphs generated by such a grammar is recognizable iff it is definable in monadic second-order logic, whereas, in general, only the “if” direction holds.     

Finite automata based on quantum logic and monadic second-order quantum logic

We introduce monadic second-order quantum logic and prove that the behaviors of finite automata based on quantum logic are precisely the quantum languages definable with sentences of our monadic secondorder quantum logic. This generalizes Büchi’s and Elgot’s fundamental theorems to quantum logic setting. We also consider first-order quantum logic and show that star-free quantum languages and aperiodic quantum languages introduced here coincide with the first-order quantum definable ones. This generalizes Sc...     

On decidability of monadic logic of order over the naturals extended by monadic predicates

A fundamental result of Büchi states that the set of monadic second-order formulas true in the structure (Nat,  <) is decidable. A natural question is: what monadic predicates (sets) can be added to (Nat,  <) while preserving decidability? Elgot and Rabin found many interesting predicates P for which the monadic theory of 〈Nat, <,  P〉 is decidable. The Elgot and Rabin automata theoretical method has been generalized and sharpened over the years and their results were extended to a variety of unary predicates. We give a sufficient and necessary model-theoretical condition for the decidability of the monadic theory of (Nat, <, P₁, … , P_n).We reformulate this condition in an algebraic framework and show that a sufficient condition proposed previously by O. Carton and W.Thomas is actually necessary. A crucial argument in the proof is that monadic second-order logic has the selection and the uniformization properties over the extensions of (Nat, <) by monadic predicates. We provide a self-contained proof of this result.     

A parallel algorithm for generating bicompatible elimination orderings of proper interval graphs

In this paper, we first show how a certain ordering of vertices, called bicompatible elimination ordering (BCO), of a proper interval graph can be used to solve efficiently several problems in proper interval graphs. We, then, propose an NC parallel algorithm (i.e., polylogarithmic-time employing a polynomial number of processors) in SIMD CRCW PRAM (Single Instruction Stream Multiple Data Stream Concurrent Read Concurrent Write Parallel Random Access Machine) model of parallel computation to compute a BCO of a proper interval graph. To the best of our knowledge, this is the first NC parallel algorithm to compute a BCO of a proper interval graph.     

Linear control of live marked graphs

Given a linear constraint on the firing vectors of a live marked graph with uncontrollable/unobservable transitions, bounded or unbounded, we apply linear programming techniques to compute the most liberal controller enforcing this constraint.     

The complexity of monadic recursion schemes: exponential time bounds

We study the computational complexity of decision problems for the class $\text{M}$ of monadic recursion schemes. By the “executability problem” for a class 't of monadic recursion schemes, we mean the problem of determining whether a given defined function symbol of a given scheme in .'t can be called during at least one computation. The executability problem for a class $\text{I}$ of very simple monadic recursion schemes is shown to require deterministic exponential time. Using arguments about executability problems and about the class $\text{I}$, a number of decision problems for. $\text{M}$ and for several of. $\text{M}$'s subclasses are shown to require deterministic exponential time. Deterministic exponential time upper bounds are also presented for several of these decision problems.     

Property analysis of logic Petri nets by marking reachability graphs

Logic Petri nets （LPNs） are suitable to describe and analyze batch processing functions and passing value indeterminacy in cooperative systems. To investigate the dynamic properties of LPNs directly, a new method for analyzing LPNs is proposed based on marking reachability graphs in this paper. Enabled conditions of transitions are obtained and a marking reachability graph is constructed. All reach- able markings can be obtained based on the graph; the fairness and reversibility of LPNs are analyzed. Moreover, the computing complexity of the enabled conditions and reachable markings can be reduced by this method. The advantages of the proposed method are illustrated by examples and analysis.     

Linear oscillation of second-order nonlinear difference equations with damped term

In this paper, we shall establish relations between the oscillation of second-order nonlinear difference equations with damped term and the oscillation of their linear limiting equations.     

Feedback control logic for forbidden-state problems of marked graphs: application to a real manufacturing system

This paper addresses the forbidden-state problem of general marked graphs with uncontrollable transitions. The models need not to be safe nor cyclic. Control requirements are expressed as the conjunction of general mutual exclusion constraints (GMEC) of markings of so-called critical places. Structural properties such as influence paths and influence zones are proposed to perform the worst-case analysis for each GMEC specification with any given initial marking when only uncontrollable transitions are allowed. Efficient solutions are proposed for the determination of the maximal uncontrollably reachable marking of any critical place, and this for many possible, more or less general, configurations of the net structure, even for the case of overlapping paths of critical places. Besides, we demonstrate that these results can be easily extended to unbounded nets and when critical places have negative weights. For the most general case, when analytical solution is not available, a linear programming approach is proposed. The great advantage of the proposed approach over existing methods is emphasized by using it to solve the supervisory control problem of the automated manufacturing system of Atelier Inter-etablissements de Productique Rhone Alpes Ouest (AIP-RAO), Lyon, France.     

Generalized finite automata theory with an application to a decision problem of second-order logic

Many of the important concepts and results of conventional finite automata theory are developed for a generalization in which finite algebras take the place of finite automata. The standard closure theorems are proved for the class of sets recognizable by finite algebras, and a generalization of Kleene's regularity theory is presented. The theorems of the generalized theory are then applied to obtain a positive solution to a decision problem of second-order logic.     

The density of truth in monadic fragments of some intermediate logics

This paper is an attempt to count the proportion of tautologies of some intermediate logics among all formulas. Our interest concentrates especially on Medvedev’s logic and its fragment over language with one propositional variable.     

Linear structure of bipartite permutation graphs and the longest path problem

The class of bipartite permutation graphs is the intersection of two well known graph classes: bipartite graphs and permutation graphs. A complete bipartite decomposition of a bipartite permutation graph is proposed in this note. The decomposition gives a linear structure of bipartite permutation graphs, and it can be obtained in O(n) time, where n is the number of vertices. As an application of the decomposition, we show an O(n) time and space algorithm for finding a longest path in a bipartite permutation graph.     

The logic of optics and the optics of logic

There have been various attempts to implement the standard logical formalism, known as “Boolean Logic”, stemming from Aristotle, the Stoics, Leibniz, Boole, and Frege, extending to the fuzzy logic developed by Zadeh [Info. Ctl. 338 (1965) 353]. That logic, isomorphic, as we now know, with the logic of electric circuitry, was not designed for optical implementation. Nor has there been a notable success in developing such an implementation. We demonstrate a new type of logic designed for implementation by coherent optics. It has the logic of Zadeh as a special case just as Zadeh's logic has the logic of Boolean algebra as a special case. Because the new logic operates over a finite set of vectors in the complex domain, we call it Vector Logic. Some Vector Logic operations are very easy to implement, but the universal “Vector NOR” or VNOR gate is quite complex. Optical Vector Logic gates are passive, so they operate at the bandwidth of the signal input and readout. And, of course, the parallel nature of many coherent optical processors can apply here as well to yield SIMD and even MIMD systems.     

Fuzzy logic and the calculi of fuzzy rules, fuzzy graphs, and fuzzy probabilities

The past few years have witnessed a rapid growth in the number and variety of applications of fuzzy logic, ranging from consumer products and industrial process control to medical instrumentation, information systems, and decision analysis. The foundations of fuzzy logic have become firmer and its impact within the basic sciences—and especially in mathematical and physical sciences—has become more visible and more substantive. And yet, there are still many misconceptions about the aims of fuzzy logic and misjudgments of its strengths and limitations.One of the common misconceptions is rooted in semantics: as a label, fuzzy logic, FL, has two different meanings. More specifically, in a narrow sense, fuzzy logic, FLn, is a logical system which aims at a formalization of approximate reasoning. In this sense, fuzzy logic is an extension of multivalued logic but its agenda is quite different from that of conventional multivalued systems.In a wide sense, fuzzy logic, FLw, is coextensive with fuzzy set theory, FST. Flw is far broader than FLn and contains Fln as one of its branches. Today, the term fuzzy logic is used predominantly in its wide sense. Thus, effectively, FL = FLw = FST.Another important point is that any field X can be fuzzified by replacing crisp sets in X by fuzzy sets. For example, through fuzzification, arithmetic can be generalized to fuzzy arithmetic, topology to fuzzy topology, control theory to fuzzy control theory, etc.In this perspective, the calculi of fuzzy rules (CFR), fuzzy graphs (CFG), and fuzzy probabilities (CFP) may be viewed as generalizations of the calculi of rules, graphs, and probabilities. The importance of CFR, CFG, and CFP derives from the fact that they play a central role in most of the applications of FL. In particular, the calculus of fuzzy graphs, which is a subset of the calculus of fuzzy rules, accounts for most of the applications of fuzzy logic in control, systems analysis, and related fields.Central to the calculus of fuzzy rules is a language referred to as the Fuzzy Dependency and Command Language (FDCL). The syntax of FDCL is concerned with the form of rules, while the semantics of FDCL is concerned with their meaning. An important issue in CFR is that of the induction of rules from observations.In CFG, a fuzzy graph is defined as the disjunction of Cartesian products of fuzzy sets. In effect, a fuzzy graph may be viewed as a compressed representation of a functional or relational dependence. Operations on fuzzy graphs play an important role in CFG.In the calculus of fuzzy probabilities, probabilities are assumed to be represented as fuzzy rather than crisp numbers. In a related way, probability distributions are represented as fuzzy graphs. A major aim of CFP is to provide a framework for linguistic decision analysis—a type of qualitative analysis in which fuzzy numbers and fuzzy graphs are employed to represent both probabilities and utilities.In an essential way, the methodologies of fuzzy rules, fuzzy graphs, and fuzzy probabilities reflect the fact that

1. (a) imprecision and uncertainty are pervasive; and

2. (b) precision and certainty carry a cost.

In the final analysis, the principal aim of these methodologies is to exploit the tolerance for imprecision and uncertainty to achieve tractability, robustness, and low solution cost.     

The logic of events

An event space is a set of instantaneous events that vary both in time and specificity. The concept of an event space provides a foundation for a logical – i.e., modular and open – approach to causal reasoning. In this article, we propose intuitively transparent axioms for event spaces. These axioms are constructive in the intuitionistic sense, and hence they can be used directly for causal reasoning in any computational logical framework that accommodates type theory. We also put the axioms in classical form and show that in this form they are adequate for the representation in terms of event trees established by Shafer [40] using stronger axioms. This revised version was published online in June 2006 with corrections to the Cover Date.     

The logic of aliasing

Summary We present a new version of Hoare's logic that correctly handles programs with aliased variables. The central proof rules of the logic (procedure call and assignment) are proved sound and complete.An earlier version of this paper appeared in the Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, 1978. This research has been partially supported by National Science Foundation grants MCS 76-14293 and MCS 76-000327