Temporal Languages for Epistemic Programs

This paper adds temporal logic to public announcement logic (PAL) and dynamic epistemic logic (DEL). By adding a previous-time operator to PAL, we express in the language statements concerning the muddy children puzzle and sum and product. We also express a true statement that an agent’s beliefs about another agent’s knowledge flipped twice, and use a sound proof system to prove this statement. Adding a next-time operator to PAL, we provide formulas that express that belief revision does not take place in PAL. We also discuss relationships between announcements and the new knowledge agents thus acquire; such relationships are related to learning and to Fitch’s paradox. We also show how inverse programs and hybrid logic each can be used to help determine whether or not an arbitrary structure represents the play of a game. We then add a past-time operator to DEL, and discuss the importance of adding yet another component to the language in order to prove completeness.     

Timed substitutions for regular signal-event languages

In the classical framework of formal languages, a refinement operation is modeled by a substitution and an abstraction by an inverse substitution. These mechanisms have been widely studied, because they describe a change in the specification level, from an abstract view to a more concrete one, or conversely. For timed systems, there is up to now no uniform notion of substitution. In this paper, we study timed substitutions in the general framework of signal-event languages, where both signals and events are taken into account. We prove that regular signal-event languages are closed under substitution and inverse substitution. To obtain these results, we use in a crucial way a “well known” result: regular signal-event languages are closed under intersection. In fact, while this result is indeed easy for languages defined by Alur and Dill’s timed automata, it turns out that the construction is much more tricky when considering the most involved model of signal-event automata. We give here a construction working on finite and infinite signal-event words and taking into account signal stuttering, unobservability of zero-duration τ-signals and Zeno runs. Note that if several constructions have been proposed in particular cases, it is the first time that a general construction is provided.     

Polynomial closure and unambiguous product

This article is a contribution to the algebraic theory of automata, but it also contains an application to Büchi’s sequential calculus. The polynomial closure of a class of languagesC is the set of languages that are finite unions of languages of the formL ₀ a ₁ L ₁ ···a _nL_n, where thea _i’s are letters and theL _i’s are elements ofC. Our main result is an algebraic characterization, via the syntactic monoid, of the polynomial closure of a variety of languages. We show that the algebraic operation corresponding to the polynomial closure is a certain Mal’cev product of varieties. This result has several consequences. We first study the concatenation hierarchies similar to the dot-depth hierarchy, obtained by counting the number of alternations between boolean operations and concatenation. For instance, we show that level 3/2 of the Straubing hierarchy is decidable and we give a simplified proof of the partial result of Cowan on level 2. We propose a general conjecture for these hierarchies. We also show that if a language and its complement are in the polynomial closure of a variety of languages, then this language can be written as a disjoint union of marked unambiguous products of languages of the variety. This allows us to extend the results of Thomas on quantifier hierarchies of first-order logic.     

Two-way automata and length-preserving homomorphisms

Closure underlength-preserving homomorphisms is interesting because of its similarity tonondeterminism. We give a characterization of NP in terms of length-preserving homomorphisms and present related complexity results. However, we mostly study the case of two-way finite automata: Let l.p.hom[n state 2DFA] denote the class of languages that are length-preserving homomorphic images of languages recognized byn-state 2DFAs. We give a machine characterization of this class. We show that any language accepted by ann-state two-wayalternating finite automaton (2AFA), or by a l-pebble 2NFA, belongs to l.p.hom[O(n ²) state 2DFA]. Moreover, there are languages in l.p.hom[n state 2DFA] whose smallest accepting 2NFA has at leastc ⁿ states (for some constantc > 1). So for two-way finite automata, the closure under length-preserving homomorphisms is much more powerful than nondeterminism. We disprove two conjectures (of Meyer and Fischer, and of Chrobak) about the state-complexity of unary languages. Finally, we show that the equivalence problems for 2AFAs (resp. 1-pebble 2NFAs) are in PSPACE, and that the equivalence problem for 1-pebble 2AFAs is in ExpSPACE (thus answering a question of Jiang and Ravikumar); it was known that these problems are hard in these two classes. We also give a new proof that alternating 1-pebble machines recognize only regular languages (which was first proved by Goralčíket al.). This research was supported in part by N.S.F. Grant DMS 8702019.     

On the regularity of circular splicing languages: a survey and new developments

Circular splicing has been introduced to model a specific recombinant behaviour of circular DNA, continuing the investigation initiated with linear splicing. In this paper we focus on the relationship between regular circular languages and languages generated by finite circular splicing systems. We survey the known results towards a characterization of the intersection between these two classes and provide new contributions on the open problem of finding this characterization. First, we exhibit a non-regular circular language generated by a circular simple system thus disproving a known result in this area. Then we give new results related to a restrictive class of circular splicing systems, the marked systems. Precisely, we review in a graph theoretical setting the recently obtained characterization of marked systems generating regular circular languages. In particular, we define a slight variant of marked systems, that is the g-marked systems, and we introduce the graph associated with a g-marked system. We show that a g-marked system generates a regular circular language if and only if its associated graph is a cograph. Furthermore, we prove that the class of g-marked systems generating regular circular languages is closed under a complement operation applied to systems. We also prove that marked systems with self-splicing generate only regular circular languages.     

More concise representation of regular languages by automata and regular expressions

We consider two formalisms for representing regular languages: constant height pushdown automata and straight line programs for regular expressions. We constructively prove that their sizes are polynomially related. Comparing them with the sizes of finite state automata and regular expressions, we obtain optimal exponential and double exponential gaps, i.e., a more concise representation of regular languages.     

Multihead Two-Way Probabilistic Finite Automata

We present properties of multihead two-way probabilistic finite automata that parallel those of their deterministic and nondeterministic counterparts. We define multihead probabilistic finite automata withlogspace constructible transition probabilities, and we describe a technique to simulate these automata by standard logspace probabilistic Turing machines. Next, we represent logspace probabilistic complexity classes as proper hierarchies based on corresponding multihead two-way probabilistic finite automata, and we show their (deterministic logspace) reducibility to the second levels of these hierarchies. We obtain a simple formula for the maximum inherent bandwidth of the configuration transition matrices associated with thek-head probabilistic finite automata processing a length-n input string. (The inherent bandwidth of the configuration transition matrices associated with an automaton processing a length-n input string is the smallest bandwidth we can get by changing the enumeration order of the automaton’s configurations.) Partially based on this relation, we find an apparently easier logspace complete problem forPL (the class of languages recognized by logspace unbounded-error probabilistic Turing machines), and we discuss possibilities for a space-efficient deterministic simulation of probabilistic automata. This research was supported by the National Science Foundation under Grant No. CDA 8822724 while the author was at the University of Rochester. An extended abstract of this paper appeared in Proceedings, Second Latin American Symposium, LATIN ’95: Theoretical Informatics, Valparaiso, Chile, April 1995.     

Formal verification of components assembly based on SysML and interface automata

We propose an approach which combines component SysML models and interface automata in order to assemble components and to verify formally their interoperability. So we propose to verify formally the assembly of components specified with the expressive and semi-formal modeling language, SysML. We specify component-based system architecture with SysML Block Definition Diagram, and the composition links between components with Internal Block Diagrams. Component’s protocols are specified with sequence diagrams, they are necessary to exploit interface automata formalism. Interface automata is a common Input Output (I/O) automata-based formalism intended to specify the signature and the protocol level of the component interfaces. We propose formal specifications for SysML semi-formal models in order to exploit interface automata approach. We also improve the interface automata approach by considering system architecture, specified with SysML, in the verification of components composition.     

Network invariants for real-time systems

We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition structures (which are similar in spirit to timed automata) and define a notion of abstraction that is safe with respect to linear temporal properties. We strengthen the notion of abstraction to allow a finite system, then called network invariant, to be an abstraction of networks of real-time systems. In general the problem of checking abstraction of real-time systems is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that one system is an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer’s protocol, using the model checker TLV. Part of this work was done during O. Grinchtein’s stay at Weizmann Institute. This author was supported by the European Research Training Network “Games”.     

Synchronizing Diachronic Uncertainty

Diachronic uncertainty, uncertainty about where an agent falls in time, poses interesting conceptual difficulties. Although the agent is uncertain about where she falls in time, this uncertainty can only obtain at a particular moment in time. We resolve this conceptual tension by providing a transformation from models with diachronic uncertainty relations into “equivalent” models with only synchronic uncertainty relations. The former are interpreted as capturing the causal structure of a situation, while the latter are interpreted as capturing its epistemic structure. The models are equivalent in the sense that agents pass through the same information sets in the same order, In this paper, we investigate how such a transformation may be used to define an appropriate notion of equivalence, which we call epistemic equivalence. Although our project is motivated by problems which have arisen in a variety of disciplines, especially philosophy and game theory, our formal development takes place within the general and flexible framework provided by epistemic temporal logic.     

Regular path queries under approximate semantics

We give a general framework for approximate query processing in semistructured databases. We focus on regular path queries, which are the integral part of most of the query languages for semistructured databases. To enable approximations, we allow the regular path queries to be distorted. The distortions are expressed in the system by using weighted regular expressions, which correspond to weighted regular transducers. After defining the notion of weighted approximate answers we show how to compute them in order of their proximity to the query. In the new approximate setting, query containment has to be redefined in order to take into account the quantitative proximity information in the query answers. For this, we define the approximate containment, and its variants k-containment and reliable contain-ment. Then, we give an optimal algorithm for deciding the k-containment. Regarding the reliable approximate containment, we show that it is polynomial time equivalent to the notorious limitedness problem in distance automata.     

On regular temporal logics with past

The IEEE standardized Property Specification Language, PSL for short, extends the well-known linear-time temporal logic LTL with so-called semi-extended regular expressions. PSL and the closely related SystemVerilog Assertions, SVA for short, are increasingly used in many phases of the hardware design cycle, from specification to verification. In this article, we extend the common core of these specification languages with past operators. We name this extension PPSL. Although all ω-regular properties are expressible in PSL, SVA, and PPSL, past operators often allow one to specify properties more naturally and concisely. In fact, we show that PPSL is exponentially more succinct than the cores of PSL and SVA. On the star-free properties, PPSL is double exponentially more succinct than LTL. Furthermore, we present a translation of PPSL into language-equivalent nondeterministic Büchi automata, which is based on novel constructions for 2-way alternating automata. The upper bound on the size of the resulting nondeterministic Büchi automata obtained by our translation is almost the same as the upper bound for the nondeterministic Büchi automata obtained from existing translations for PSL and SVA. Consequently, the satisfiability problem and the model-checking problem for PPSL fall into the same complexity classes as the corresponding problems for PSL and SVA.     

Compositional synthesis of asynchronous automata

Asynchronous automata are a model of communication processes with a control structure distributed on a set P of processes, global initializations and global accepting conditions. The well-known theorem of Zielonka states that they recognize exactly the class of regular Mazurkiewicz trace languages. The corresponding synthesis problem is, given a global specification A of any regular trace language L, to build an asynchronous automaton that recognizes L, automatically. Yet, all such existing constructions are quite involved and yield an explosion of the number of states in each process, which is exponential in both the sizes of A and P. In this paper, we introduce the particular case of distributed asynchronous automata, which require that the initializations and the accepting conditions are distributed as well. We present an original technique based on simple compositions/decompositions of these distributed asynchronous automata that results in the construction of smaller non-deterministic asynchronous automata: now, the number of states in each process is only polynomial in the size of A, but is still exponential in the size of P.     

One-Unambiguous Regular Languages

The ISO standard for the Standard Generalized Markup Language (SGML) provides a syntactic meta-language for the definition of textual markup systems. In the standard, the right-hand sides of productions are based on regular expressions, although only regular expressions that denote words unambiguously, in the sense of the ISO standard, are allowed. In general, a word that is denoted by a regular expression is witnessed by a sequence of occurrences of symbols in the regular expression that match the word. In an unambiguous regular expression as defined by Booket al.(1971,IEEE Trans. Comput.C-20(2), 149–153), each word has at most one witness. But the SGML standard also requires that a witness be computed incrementally from the word with a one-symbol lookahead; we call such regular expressions 1-unambiguous. A regular language is a 1-unambiguouslanguage if it is denoted by some 1-unambiguous regular expression. We give a Kleene theorem for 1-unambiguous languages and characterize 1-unambiguous regular languages in terms of structural properties of the minimal deterministic automata that recognize them. As a result we are able to prove the decidability of whether a given regular expression denotes a 1-unambiguous language; if it does, then we can construct an equivalent 1-unambiguous regular expression in worst-case optimal time.     

Epistemic logic and logical omniscience: A survey

This survey brings together a collection of epistemic logics and discusses their approaches in alleviating the logical omniscience problem. Of particular note is the logic of implicit and explicit belief. Explicit belief refers to information actively held by an agent, while implicit belief refers to the logical consequence of explicit belief. Ramifications of Levesque's logic include nonstandard epistemic logic and the logics of awareness and local reasoning. Models of nonstandard epistemic logic are defined with respect to nonstandard proportional logic to weaken its semantics. In the logic of awareness, an agent can only believe a concept that it is aware of. Closely related to awareness are S-1 and S-3 epistemic operators which can be used to model skeptical and credulous agents. The logic of local reasoning provides a semantics for representing the fact that agents can have different clusters of beliefs which may contradict each other. Other variations include epistemic structures which are generalizations of the logic of local reasoning and fusion epistemic models which provide an account that agents can combine information conjunctively or disjunctively. Another closely related approach is the logic of explicit propostions which captures the insight that agents can hold beliefs independently without putting them together. © 1997 John Wiley & Sons, Inc.     

A continuum of discrete systems

We show how to regard covered logic programs as cellular automata. Covered logic programs are ones for which every variable occurring in the body of a given clause also occurs in the head of the same clause. We generalize the class of register machine programs to permit negative literals and characterize the members of this class of programs as n-state 2-dimensional cellular automata. We show how monadic covered programs, the class of which is computationally universal, can be regarded as 1-dimensional cellular automata. We show how to continuously (and differentiably) deform 1-dimensional cellular automata from one to another and understand the arrangement of these cellular automata in a separable Hilbert space over the real numbers. The embedding of the cellular automata of fixed radius r is a linear mapping into R^{2 2r+1} in which a cellular automaton's transition function is the attractor of a state-governed iterated function system of affine contraction mappings. The class of covered monadic programs having a particular fixed point has a uniform arrangement in an affine subspace of the Hilbert space l². Furthermore, these programs are construable as almost everywhere continuous functions from the unit interval {x | 0 ≤ x ≤ 1} to the real numbers R. As one consequence, in particular, we can define a variety of natural metrics on the class of these programs. Moreover, for each program in this class, the set of initial segments of the program's fixed points, with respect to an ordering induced by the program's dependency relation, is a regular set. This revised version was published online in June 2006 with corrections to the Cover Date.     

Power of interconnections and of nondeterminism in regularY-tree systolic automata

The increase of computational power due to additions of some horizontal interconnections between neighboring nodes of binary trees is investigated using the concept of systolic automata over so-called 7-trees with one-directional, bottom-to-root, flow of computation.Y-trees are obtained from binary trees by connecting some neighboring pairs of nodes at the same level that are not brothers.We introduce the concept of systolic automata on regularY-trees in column normal form and prove that any systolic automaton on regularY-trees is equivalent to one in the column normal form. We then fully characterize those regularY-trees over which the class of languages recognized by nondeterministic automata is the same as for deterministic automata. An analogous result is obtained for stability. Furthermore, we show that superstable deterministic systolic automata over regularY-trees recognize only regular languages. Finally, several closure properties of and relations between classes of languages accepted by systolic automata over differentY-trees are studied.The preliminary version of this paper was presented at the 2nd International Colloquium on Words, Languages, and Combinatorics in Kyoto, Japan, August 1992. This work has been partially supported by the Ministero dell' Universitá e della Ricerca Scientifica e Tecnologica of Italy and by a grant from the Slovak Academy of Sciences, Bratislava, Slovakia. The second author is on a leave of absence from the Institute of Informatics, Slovak Academy of Sciences, Bratislava, Slovakia.     

A general approach for building combinational P automata

In traditional automata theory, the closure with respect to certain operations is one of the most investigated properties, especially the methods of constructing automata for certain operations among the given sub-automata. However, up to now less effort has been addressed to this question for P automata. As an improvement on earlier results, we introduce P automata with communication and active membrane rules working in the initial mode (CAIP). We present methods for constructing automata that recognize the Union, the Concatenation, the Kleene Closure, or the ω Closure of the given languages which are represented by some P automata. We also show that for any language denoted by a regular expression, we can readily construct a CAIP automaton corresponding to it.     

Some Properties of Iterated Languages

A special kind of substitution on languages called iteration is presented and studied. These languages arise in the application of semantic automata to iterations of generalized quantifiers. We show that each of the star-free, regular, and deterministic context-free languages are closed under iteration and that it is decidable whether a given regular or determinstic context-free language is an iteration of two such languages. This result can be read as saying that the van Benthem/Keenan ‘Frege Boundary’ is decidable for large subclasses of natural language quantifiers. We also determine the state complexity of iteration of regular languages.