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