Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday
In October 1997, whilst touching up this text, exactly 50 years had past since I was accepted for graduate studies under P.S. Novikov. I started then to study and do research in logic and computability, which developed, as time will show, into research in Theoretical Computer Science (TCS). After my emigration (in December 1980) from the Soviet Union (SU), I was encouraged by colleagues to...
In his early memoirs, Trakhtenbrot told several stories. The greater part is an intellectual history of Soviet research in theoretical computer science from the 1950’s to the late 70’s. A second story – of academic and political disputes that shaped the course of Soviet research in the area – is briefly indicated. Finally, there is a laconic suggestion of the scientific life of a gifted, prolific...
According to the Mathematics Genealogy Project (at http://genealogy. math.ndsu.nodak.edu ), Trakhtenbrot’s ancestral dag is rooted in Otto Mencke (who received his degree in 1666, but whose advisor is not listed).
The Logic of Proofs LP captures the invariant propositional properties of proof predicates t is a proof of F with a set of operations on proofs sufficient for realizing the whole modal logic S4 and hence the intuitionistic logic IPC. Some intuitive properties of proofs, however, are not invariant and hence not present in LP. For example, the choice function ‘+’ in LP, which is specified by the condition...
In model-driven development of reactive systems, statecharts are widely used for formal description of their behavior, providing a sound basis for verification, testing and code generation. The paper presents an approach for dynamic analysis of reactive systems via run-time monitoring of code generated from statechart-based models. The core of the approach is automatic creation of monitoring statecharts...
We present a new unified framework for formalizations of axiomatic set theories of different strength, from rudimentary set theory to full ZF. It allows the use of set terms, but provides a static check of their validity. Like the inconsistent “ideal calculus” for set theory, it is essentially based on just two set-theoretical principles: extensionality and comprehension (to which we add ∈-induction...
Propositional logics in general, considered as a set of sentences, can be undecidable even if they have “nice” representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple—at worst NP. Moreover, finite-valued semantics...
In this paper a sequence of model transformation languages L0, L1, L2 is defined. The first language L0 is very simple, and for this language it is easy to build an efficient compiler to C++. The next language L1 is an extension of L0, and it contains powerful pattern definition facilities. The last language L2 is of sufficiently high level and can be used for implementation of traditional pattern-based...
We show that propositional dynamic logic and the modal μ-calculus are closed under product modalities, as defined in current dynamic-epistemic logics. Our analysis clarifies the latter systems, while also raising some new questions about fixed-point logics.
Fields and division rings are not algebras in the sense of “Universal Algebra”, as inverse is not a total function. Mending the inverse by any definition of 0− 1 will not suffice to axiomatize the axiom of inverse x − 1·x = 1, by an equation. In particular the theory of fields cannot be used for specifying the abstract data type of the rational numbers. We define equational theories...
Sets play a key role in foundations of mathematics. Why? To what extent is it an accident of history? Imagine that you have a chance to talk to mathematicians from a far-away planet. Would their mathematics be set-based? What are the alternatives to the set-theoretic foundation of mathematics? Besides, set theory seems to play a significant role in computer science; is there a good justification for...
The Church-Turing Thesis has been the subject of many variations and interpretations over the years. Specifically, there are versions that refer only to functions over the natural numbers (as Church and Kleene did), while others refer to functions over arbitrary domains (as Turing intended). Our purpose is to formalize and analyze the thesis when referring to functions over arbitrary domains. ...
Generalized Categorial Dependency Grammars (gCDG) studied in this paper are genuine categorial grammars expressing projective and discontinuous dependencies, stronger than CF-grammars and non-equivalent to mild context-sensitive grammars. We show that gCDG are parsed in polynomial time and enjoy good mathematical properties.
Probabilistic systems of interacting intelligent agents are considered. They have two sources of uncertainty: uncertainty of communication channels and uncertainty of actions. We show how such systems can be polynomially transformed to finite state Markov chains. This allows one to transfer known results on verifying temporal properties of the finite state Markov chains to the probabilistic multi-agent...
A sequence of graphs G n is iteratively constructible if it can be built from an initial labeled graph by means of a repeated fixed succession of elementary operations involving addition of vertices and edges, deletion of edges, and relabelings. Let G n be a iteratively constructible sequence of graphs. In a recent paper, [27],...
Size (the number of states) of finite probabilistic automata with an isolated cut-point can be exponentially smaller than the size of any equivalent finite deterministic automaton. The result is presented in two versions. The first version depends on Artin’s Conjecture (1927) in Number Theory. The second version does not depend on conjectures but the numerical estimates are worse. In both versions...
Ordinary Kripke models are not reactive. When we evaluate (test/measure) a formula A at a model m, the model does not react, respond or change while we evaluate. The model is static and unchanged. This paper studies Kripke models which react to the evaluation process and change themselves during the process. The additional device we add to Kripke semantics to make it reactive is to allow the accessibility...
We construct a model without precipitous ideals but so that for each there is a normal ideal over with generic ultrapower wellfounded up to the image of τ.
We survey some of the main results regarding the complexity and expressive power of Live Sequence Charts (LSCs). We first describe the two main semantics given to LSCs: a trace-based semantics and an operational semantics. The expressive power of the language is then examined by describing translations into various temporal logics. Some limitations of the language are also discussed. Finally, we survey...