Fundamenta Informaticae - Volume 62, issue 1

Authors: Trakhtenbrot, Boris A.

Article Type: Other

Citation: Fundamenta Informaticae, vol. 62, no. 1, pp. v-vii, 2004

Authors: Hirshfeld, Yoram | Rabinovich, Alexander

Article Type: Research Article

Abstract: Over the last fifteen years formalisms for reasoning about metric properties of computations were suggested and discussed. First as extensions of temporal logic, ignoring the framework of classical predicate logic, and then, with the authors' work, within the framework of monadic logic of order. Here we survey our work on metric logic comparing it to the previous work in the field. We define a quantitative temporal logic that is based on a simple modality within the …framework of monadic predicate Logic. Its canonical model is the real line (and not an omega-sequence of some type). It can be interpreted either by behaviors with finite variability or by unrestricted behaviors. For finite variability models it is as expressive as any logic suggested in the literature. For unrestricted behaviors our treatment is new. In both cases we prove decidability and complexity bounds using general theorems from logic (and not from automata theory). Show more

Citation: Fundamenta Informaticae, vol. 62, no. 1, pp. 1-28, 2004

Authors: Slissenko, Anatol

Article Type: Research Article

Abstract: This paper is a survey of research of my colleagues and myself aimed at developing a comprehensive logical framework for the verification of real-time distributed systems. The framework is based on predicate logics with explicit time. To choose such a logic we pursue two goals: first, to make formalization of verification problems rather direct, without unjustified simplifications, and second, to have a logic which permits to describe decidable classes of the verifications problem covering the particular …problems we are interested in. Notice that our intention is not to introduce new specification languages, but work directly with those of the user. In this paper we describe First Order Timed Logic (FOTL) that is sufficient to express the main part of verification of systems without uncertainty. The time is continuous (the formalism work as well for discrete time — in our context this case is less interesting and less efficient from algorithmic viewpoint). We give examples of problems that can be treated, describe how to represent runs of programs in FOTL, introduce decidable classes, discuss aspects of practical efficiency. We conclude with open questions. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 1, pp. 29-67, 2004

Authors: Trakhtenbrot, B.A.

Article Type: Research Article

Abstract: Paradigms, in which continuous time is involved in cooperation with, or instead of, discrete time appear now in different areas related to automata, logic and interaction. Unfortunately, they are accompanied by a plethora of definitions, terminology and notation, which is not free of ad-hoc and ambiguous decisions. The overuse of definitions from scratch of intricate notions without a previous, explicit core of basic generic notions engenders further models and formalisms, and it is not clear where …to stop. Hence (quoting J.Hartmanis), the challenge "to isolate the right concepts, to formulate the right models, and to discard many others, that do not capture the reality we want to understand...". We undertake this challenge wrt some automata-theoretic concepts and issues that appear in the literature on continuous-time circuits and hybrid automata, by keeping to the following guidelines: 1. Building on Basic Automata Theory. 2. Coherence with original or potential discrete-time paradigms, whose continuous-time analogs and/or mutants we would like to understand. 3. Functions, notably input/output behavior of devices, should not be ignored in favor of sets (languages) accepted by them. The paper outlines the approach which emerged in previous research [PRT, RT, T3, T4, R] and in teaching experience [T0, T2]. As an illustration we offer a precise explanation of the evasive relationship between hybrid automata, constrained automata} and control circuits. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 1, pp. 69-121, 2004

Authors: Pardo, D. | Rabinovich, A. | Trakhtenbrot, B.A.

Article Type: Research Article

Abstract: To what mathematical models do digital computer circuits belong? In particular: (i) (Feedback reliability.) Which cyclic circuits should be accepted? In other words, under which conditions is causally faithful the propagation of signals along closed cycles of the circuit? (ii) (Comparative power and completeness.) What are the appropriate primitives upon which circuits may be (or should be) assembled? There are well-known answers to these questions for circuits operating in discrete time, and they point on the exclusive …role of the unit-delay primitive. For example: (i) If every cycle in the circuit N passes through a delay, then N is feedback reliable. (ii) Every finite-memory operator F is implementable in a circuit over unit-delay and pointwise boolean gates. In what form, if any, can such phenomena and results be extended to circuits operating in continuous time? This is the main problem considered (and, hopefully, solved to some extent) in this paper. In order to tackle the problems one needs more insight into specific properties of continuous time signals and operators that are not visible at discrete time. Show more

Citation: Fundamenta Informaticae, vol. 62, no. 1, pp. 123-137, 2004