Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

In this paper we prove theorems on the interpretability of the first-order temporal logics LTL and TL into Fork Algebras. This result is part of a research project on the interpretability of logics in Fork Algebras, and has important applications towards the relational specification of properties of systems within the Ar gentum tool. © 2005 Elsevier Inc. All rights reserved.

Registro:

Documento: Artículo
Título:Interpretability of first-order linear temporal logics in fork algebras
Autor:Frias, M.F.; Pombo, C.G.L.
Filiación:Department of Computer Science, School of Exact and Natural Sciences, Ciudad Universitaria, Buenos Aires, 1428, Argentina
CONICET, Argentina
Palabras clave:Fork algebras; Interpretability; Software verification; Temporal logics; Fork algebras; Interpretability; Software verification; Temporal logics; Computer software; Formal logic; Mathematical programming; Theorem proving; Algebra
Año:2006
Volumen:66
Número:2
Página de inicio:161
Página de fin:184
DOI: http://dx.doi.org/10.1016/j.jlap.2005.04.005
Título revista:Journal of Logic and Algebraic Programming
Título revista abreviado:J. Logic. Algebraic Program.
ISSN:15678326
CODEN:JLAPA
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15678326_v66_n2_p161_Frias

Referencias:

  • Brink Kahl, W.C., Schmidt, G., (1997) Relational Methods in Computer Science, , Springer Wien-New York
  • Burris, S., Sankappanavar, H.P., A course in universal algebra (1981) Graduate Texts in Mathematics, 78. , Springer-Verlag
  • Chin, L.H., Tarski, A., Distributive and modular laws in the arithmetic of relation algebras (1951) University of California Publications in Mathematics, 1 (9), pp. 341-384
  • Clarke, E.M., Emerson, E.A., Design and synthesis of synchronisation skeletons using branching time temporal logic (1981) LNCS 131, pp. 52-71. , D. Kozen, Logics of programs, Springer-Verlag
  • Emerson, E.A., Temporal and modal logic (1990) Handbook of Theoretical Computer Science, , J. van Leeuwen Elsevier Science Publishers Amsterdam
  • De Morgan, A., (1966) On the Syllogism, and other Logical Writings, , Yale University Press
  • Frias, M.F., Fork algebras in algebra (2002) Advances in Logic, 2. , World Scientific Publishing Co
  • Frias, M.F., Baum, G.A., Haeberer, A.M., Fork algebras in algebra, logic and computer science (1997) Fundamenta Informaticae, 32, pp. 1-25
  • Frias, M.F., Baum, G.A., Maibaum, T.S.E., Interpretability of first-order dynamic logic in a relational calculus (2002) LNCS, 2561, pp. 66-80. , Proceedings of RelMiCS 6, Springer-Verlag
  • Frias, M.F., Orłowska, E., A proof system for fork algebras and its applications to reasoning in logics based on intuitionism (1997) Logique et Analyse, 150-152, pp. 239-284. , 151
  • Frias, M.F., Orłowska, E., Equational reasoning in non-classical logics (1998) Journal of Applied Non Classical Logic, 8 (12), pp. 27-66
  • Frias, M.F., Pombo, C.G.L., Time is on my Side (2003) RelMiCS'03, , in abstracts of Malente, Germany
  • Löwenheim, L., Über Möglichkeiten im Relativkalkül (1915) Mathematische Annalen, 76, pp. 447-470
  • Lyndon, R., The representation of relational algebras (1950) Annals of Mathematics (Series 2), 51, pp. 707-729
  • Lyndon, R., The representation of relational algebras, Part II (1956) Annals of Mathematics (Series 2), 63, pp. 294-307
  • Maddux, R.D., Finitary algebraic logic (1989) Zeitschr. F. Math. Logik und Grundlagen D. Math., 35, pp. 321-332
  • Manna, Z., Pnueli, A., (1991) The Temporal Logic of Reactive and Concurrent Systems - Specification, , Springer-Verlag
  • Manna, Z., Pnueli, A., (1995) Temporal Verification of Reactive Systems - Safety, , Springer-Verlag New York
  • Orłowska, E., Relational Formalisation of Nonclassical Logics, , Chapter 6 of [1]
  • Peirce, Ch.S., (1933) Collected Papers, , Harvard University Press Cambridge
  • Schlingloff, H., Heinle, W., Relation Algebra and Modal Logics, , Chapter 5 of [1]
  • Schröder, E.F.W.K., Vorlesungen über die algebra der logik (exacte Logik) (1895) Algebra und Logik der Relative, Part I, 3. , Leipzig
  • Tarski, A., On the calculus of relations (1941) Journal of Symbolic Logic, 6, pp. 73-89
  • Tarski, A., Lattice-theoretic fixpoint theorem and its applications (1955) Pacific Journal of Mathematics, 5, pp. 285-309
  • Tarski, A., Givant, S., (1987) A Formalization of Set Theory Without Variables, 41. , American Mathematical Society Colloquium Publications American Mathematical Society
  • Von Karger, B., Temporal algebra (1998) Mathematical Structures in Computer Science, 8 (3), pp. 277-320
  • Von Karger, B., Berghammer, R., A relational model for temporal logic (1998) Logic Journal of the IGPL, 6 (2), pp. 157-173

Citas:

---------- APA ----------
Frias, M.F. & Pombo, C.G.L. (2006) . Interpretability of first-order linear temporal logics in fork algebras. Journal of Logic and Algebraic Programming, 66(2), 161-184.
http://dx.doi.org/10.1016/j.jlap.2005.04.005
---------- CHICAGO ----------
Frias, M.F., Pombo, C.G.L. "Interpretability of first-order linear temporal logics in fork algebras" . Journal of Logic and Algebraic Programming 66, no. 2 (2006) : 161-184.
http://dx.doi.org/10.1016/j.jlap.2005.04.005
---------- MLA ----------
Frias, M.F., Pombo, C.G.L. "Interpretability of first-order linear temporal logics in fork algebras" . Journal of Logic and Algebraic Programming, vol. 66, no. 2, 2006, pp. 161-184.
http://dx.doi.org/10.1016/j.jlap.2005.04.005
---------- VANCOUVER ----------
Frias, M.F., Pombo, C.G.L. Interpretability of first-order linear temporal logics in fork algebras. J. Logic. Algebraic Program. 2006;66(2):161-184.
http://dx.doi.org/10.1016/j.jlap.2005.04.005