Fundamenta Informaticae - Volume 24, issue 4

Authors: Kutty, G. | Moser, L.E. | Melliar-Smith, P.M. | Ramakrishna, Y.S. | Dillon, L.K.

Article Type: Research Article

Abstract: Interval logic has been introduced as a temporal logic that provides higher-level constructs and an intuitive graphical representation, making it easier in interval logic than in other temporal logics to specify and reason about concurrency in software and hardware designs. In this paper we present axiomatizations for two propositional interval logics and relate these logics to Until Temporal Logic. All of these logics are discrete linear-time temporal logics with no next operator. The next operator obstructs the use of hierarchical abstraction and refinement, and makes reasoning about concurrency difficult.

DOI: 10.3233/FI-1995-2441

Citation: Fundamenta Informaticae, vol. 24, no. 4, pp. 313-331, 1995

Authors: Magott, Jan

Article Type: Research Article

Abstract: In the field of distributed computer systems, in order to specify, verify, and implement systems formally, Formal Description Techniques have been developed. Specification language Estelle, which is an ISO standard, is one of these techniques. Purpose of the present paper is to create a method of performance evaluation for the language Estelle that is based on Petri net methodology. The paper is oriented towards partially automatic generation of performance model for a distributed system - having Estelle specification of this system. A method for finding the performance characteristics of system defined in Estelle is given too.

DOI: 10.3233/FI-1995-2442

Citation: Fundamenta Informaticae, vol. 24, no. 4, pp. 333-357, 1995

Authors: Seda, Anthony Karel

Article Type: Research Article

Abstract: We introduce topologies on spaces of interpretations which extend and generalise the query and positive query topologies of Batarekh and Subrahmanian. We study continuity in these topologies of the immediate consequence map associated with any normal logic program and provide necessary and sufficient conditions for continuity to hold. We relate these ideas to (i) computational power of programs; (ii) canonical programs; (iii) the declarative semantics of definite programs; (iv) Maher's down continuous programs; (v) the decency thesis of Jaffar, Lassez and Maher, and (vi) compactness of sets of fixed points and models.

DOI: 10.3233/FI-1995-2443

Citation: Fundamenta Informaticae, vol. 24, no. 4, pp. 359-386, 1995

Authors: Ramakrishna, Y.S.

Article Type: Research Article

Abstract: The Temporal Logic of Actions (TLA) devised by Lamport is a logic for proving the correctness of concurrent systems. A distinctive feature of the logic is the use of “action formulae” to encode the “before-after” behaviour of transitions, a feature that is especially suitable for Lamport's transition-axiom method. Abadi has given a complete axiomatization for the propositional fragment of this logic, and conjectured that its validity problem may be in PSPACE. In this paper we confirm that conjecture. In fact we show that the validity problem for TLA is PSPACE-complete. For this we give a space-optimal automata-theoretic decision procedure for …TLA. Our result is obtained with respect to a logic which is a conservative extension of Lamport's TLA. Thus our decision procedure applies to the more restricted logic. We show how the automata-theoretic framework handles abstraction, as used in TLA, a feature considered useful for hierarchical and compositional reasoning. Show more

DOI: 10.3233/FI-1995-2444

Citation: Fundamenta Informaticae, vol. 24, no. 4, pp. 387-405, 1995

Authors: Gasquet, Olivier

Article Type: Research Article

Abstract: We prove that a natural and simple predicate modal logic with the Barcan formula, namely QBF-KD plus the axiom of density, is not Kripke complete. Although incompleteness results are known in Kripke semantics, most of the methods used can only apply to logics stronger than QBF-S4 as they are based in a translation from intermediate logics. We give here an original proof of this incompleteness result.

DOI: 10.3233/FI-1995-2445

Citation: Fundamenta Informaticae, vol. 24, no. 4, pp. 407-415, 1995