×

Semiring neighbours: an algebraic embedding and extension of neighbourhood logic. (English) Zbl 1277.03028

Romijn, Judi (ed.) et al., Proceedings of the doctoral symposium affiliated with the fifth integrated formal methods conference (IFM 2005), Eindhoven, The Netherlands, November 29, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 191, 49-72 (2007).
Summary: In 1996 Zhou and Hansen proposed a first-order interval logic called neighbourhood logic (NL) for specifying liveness and fairness of computing systems and defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou developed a sound and relatively complete duration calculus as an extension of NL.
We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get many properties for free. As one important result we obtain that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. Furthermore, we discuss other interval operations like Allen’s 13 relations between intervals and their relationship to semiring neighbours. Then we present some possible interpretations for neighbours beyond interval settings. Here we discuss for example reachability in graphs and applications to hybrid systems. At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirings to Kleene algebras and \(\omega\) algebras. These extensions are useful for formulating properties of repetitive procedures like loops.
For the entire collection see [Zbl 1276.68029].

MSC:

03B70 Logic in computer science
03B44 Temporal logic
06F07 Quantales
16Y60 Semirings
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

CalcCheck
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Allen, J. F., Maintaining Knowledge about Temporal Intervals, Communications of the ACM, 26, 11, 822-843 (1983) · Zbl 0519.68079
[2] Allen, J. F.; Hayes, P., A Common-sense Theory of Time, (Proceedings of the 9th International Joint Conference on Artificial Intelligence (1985), Morgan Kaufmann), 528-531
[3] Backhouse, R., Galois Connections and Fixed Point Calculus, (Algebraic and Coalgebraic Methods in the Mathematics of Program Construction (2002), Springer), 89-148 · Zbl 1065.68030
[4] Conway, J. H., Regular Algebra and Finite Machines (1971), Chapman and Hall · Zbl 0231.94041
[5] Desharnais, J.; Mölle, B., Characterizing Determinacy in Kleene Algebra, Special Issue on Relational Methods in Computer Science, Information Sciences - An International Journal, 139, 253-273 (2001) · Zbl 1004.68105
[6] J. Desharnais, B. Möller and G. Struth: Kleene Algebra with Domain. ACM Trans. Computational Logic (to appear 2006). Preliminary version: Universität Augsburg, Institut für Informatik, Report No. 2003-07, June 2003; J. Desharnais, B. Möller and G. Struth: Kleene Algebra with Domain. ACM Trans. Computational Logic (to appear 2006). Preliminary version: Universität Augsburg, Institut für Informatik, Report No. 2003-07, June 2003
[7] Desharnais, J.; Möller, B.; Struth, G., Modal Kleene Algebra and Applications - A Survey, J. Relational Methods in Computer Science, 1, 93-131 (2004)
[8] Dutertre, B., Complete Proof Systems for First-order Interval Temporal Logic, (Tenth Annual IEEE Symb. on Logic in Computer Science (1995), IEEE Press), 36-43
[9] Golan, J. S., The Theory of Semirings with Applications in Mathematics and Theoretical Computer Science (1992), Longman · Zbl 0780.16036
[10] Halpern, J. Y.; Moszkowski, B.; Manna, Z., A Hardware Semantics Based on Temporal Intervals, (Diaz, J., ICALP’83. ICALP’83, Lecture Notes in Computer Science, 154 (1983), Springer), 278-291
[11] Gries, D.; Schneider, F. B., A Logical Approach to Discrete Math (1993), Springer · Zbl 0861.03001
[12] J.Y. Halpern and Y. Shoham. A Propositional Modal Logic of Time Intervals. Proceedings of the First IEEE Symposium on Logic in Computer Science. IEEE Press, Piscataway, NJ, 279-292; J.Y. Halpern and Y. Shoham. A Propositional Modal Logic of Time Intervals. Proceedings of the First IEEE Symposium on Logic in Computer Science. IEEE Press, Piscataway, NJ, 279-292 · Zbl 0799.68175
[13] Hebisch, U.; Weinert, H. J., Semirings - Algebraic Theory and Applications in Computer Science (1998), World Scientific: World Scientific Singapur · Zbl 0934.16046
[14] P. Höfner. An Algebraic Semantics for Duration Calculus. Proc. 10th ESSLLI Student Session, Edinburgh, 2005, 99-111. Extended version: From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus. Universität Augsburg, Institut für Informatik, Report No. 2005- 05, March 2005; P. Höfner. An Algebraic Semantics for Duration Calculus. Proc. 10th ESSLLI Student Session, Edinburgh, 2005, 99-111. Extended version: From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus. Universität Augsburg, Institut für Informatik, Report No. 2005- 05, March 2005
[15] Höfner, P.; Möller, B., Lazy Semiring Neighbours and some Applications, (Schmidt, R., RelMiCS /AKA 2006. RelMiCS /AKA 2006, Lecture Notes in Computer Science, 4136 (2006), Springer), 207-221 · Zbl 1134.68408
[16] Höfner, P.; Möller, B., Towards an Algebra of Hybrid Systems, (MacCaull, W.; Winter, M.; Duentsch, I., Relational Methods in Computer Science. Relational Methods in Computer Science, Lecture Notes in Computer Science, 3929 (2006), Springer), 121-133 · Zbl 1185.68431
[17] B. von Karger: Temporal Algebra. Habilitation thesis, University of Kiel 1997; B. von Karger: Temporal Algebra. Habilitation thesis, University of Kiel 1997
[18] Kozen, D., Kleene Algebra with Tests, Trans. Prog. Languages and Systems, 19, 3, 427-443 (1997)
[19] B. Möller. Complete Tests do not Guarantee Domain. Universität Augsburg, Institut für Informatik, Report No. 2005-06, March 2005; B. Möller. Complete Tests do not Guarantee Domain. Universität Augsburg, Institut für Informatik, Report No. 2005-06, March 2005
[20] Mölle, B., Lazy Kleene algebra, (Kozen, D., Mathematics of program construction. Mathematics of program construction, Lecture Notes in Computer Science, 3125 (2004), Springer), 252-273, Previous version: · Zbl 1106.68065
[21] B. Möller. Residuals and Detachments. Universität Augsburg, Institut für Informatik, Report No. 2005- 20, December 2005; B. Möller. Residuals and Detachments. Universität Augsburg, Institut für Informatik, Report No. 2005- 20, December 2005
[22] Möller, B.; Höfner, P.; Struth, G., Quantales and Temporal Logics, (Johnson, M.; Vene, V., Algebraic Methodology and Software Technology. Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, 3929 (2006), Springer), 263-277 · Zbl 1235.03051
[23] S. Roy and C.C. Zhou. Notes on Neighbourhood Logic. Technical Report 97, The United Nations University UNU/IIST, February 1997; S. Roy and C.C. Zhou. Notes on Neighbourhood Logic. Technical Report 97, The United Nations University UNU/IIST, February 1997
[24] Venema, Y., A Modal Logic for Chopping Intervals, J. of Logic and Computation, 1, 4, 453-476 (1990) · Zbl 0744.03022
[25] Zhou, C. C.; Van Hung, D.; Xiaoshan, Li, A Duration Calculus with Infinite Intervals, (Fundamentals of Computation Theory (1995)), 16-41 · Zbl 1508.68228
[26] Zhou, C. C.; Hansen, M. R., Duration Calculus - A Formal Approach to Real-Time Systems, Monographs in Theoretical Computer Science (1996), Springer
[27] Zhou, C. C.; Hansen, M. R., An Adequate First Order Interval Logic, Lecture Notes in Computer Science, 1536, 584-608 (1998)
[28] C.C. Zhou and M.R. Hansen. An Adequate First Order Interval Logic. Technical Report 91, The United Nations University UNU/IIST, 1996; C.C. Zhou and M.R. Hansen. An Adequate First Order Interval Logic. Technical Report 91, The United Nations University UNU/IIST, 1996
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.