A Graphical Proof Theory of Logical Time

[en] Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV.

Disciplines :

Computer science

Author, co-author :

ACCLAVIO, Matteo ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

HORNE, Ross James ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

MAUW, Sjouke ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

Straßburger, Lutz; Inria-Saclay, Palaiseau, France

External co-authors :

yes

Language :

English

Title :

A Graphical Proof Theory of Logical Time

Publication date :

2022

Event name :

7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Event place :

Haifa, Israel

Event date :

August 2-5, 2022

Audience :

International

Main work title :

Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Editor :

Felty, Amy P.

Publisher :

Schloss Dagstuhl -- Leibniz-Zentrum fur Informatik, Germany

ISBN/EAN :

978-3-95977-233-4

Collection name :

Leibniz International Proceedings in Informatics

Pages :

22:1-22:25

Peer reviewed :

Peer reviewed

Focus Area :

Security, Reliability and Trust

Additional URL :

https://drops.dagstuhl.de/opus/volltexte/2022/16303

Available on ORBilu :

since 19 January 2023

Statistics

Number of views

55 (1 by Unilu)

Number of downloads

15 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenAlex citations

Bibliography

Matteo Acclavio, Ross Horne, and Lutz Straßburger. Logic beyond formulas: A proof system on graphs. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’20, pages 38–52, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3373718.3394763.
Matteo Acclavio, Ross Horne, and Lutz Straßburger. An analytic propositional proof system on graphs. Logical Methods in Computer Science, 2022. to appear. doi:10.48550/arXiv. 2012.01102.
Matteo Acclavio and Roberto Maieli. Generalized connectives for multiplicative linear logic. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of LIPIcs, pages 6:1–6:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi:10.4230/LIPIcs.CSL.2020.6.
Andrea Aler Tubella. A study of normalisation through subatomic logic. PhD thesis, University of Bath, 2017.
Andrea Aler Tubella and Lutz Straßburger. Introduction to deep inference. Lecture, August 2019. URL: https://hal.inria.fr/hal-02390267.
Denis Bechet, Philippe de Groote, and Christian Retoré. A complete axiomatisation of the inclusion of series-parallel partial orders. In H. Common, editor, Rewriting Techniques and Applications, RTA 1997, volume 1232 of LNCS, pages 230–240. Springer, 1997.
Carmen Bruckmann, Peter F. Stadler, and Marc Hellmuth. From modular decomposition trees to rooted median graphs. Discrete Applied Mathematics, 310:1–9, 2022. doi:10.1016/j. dam.2021.12.017.
Paola Bruscoli. A purely logical account of sequentiality in proof search. In Peter J. Stuckey, editor, Logic Programming, pages 302–316, Berlin, Heidelberg, 2002. Springer. doi:10.1007/ 3-540-45619-8_21.
Cameron Calk, Anupam Das, and Tim Waring. Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs, 2020. doi:10.48550/arXiv.2004.12941.
Vincent Danos and Laurent Regnier. The structure of the multiplicatives. Arch. Math. Log., 28(3):181–203, 1989. doi:10.1007/BF01622878.
Yuxin Deng, Robert J. Simmons, and Iliano Cervesato. Relating reasoning methodologies in linear logic and process algebra. Mathematical Structures in Computer Science, 26(5):868–906, 2016. doi:10.1017/S0960129514000413.
Pierre-Malo Deniélou and Nobuko Yoshida. Buffered communication analysis in distributed multiparty sessions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 343–357, Berlin, Heidelberg, 2010. Springer. doi:10.1007/ 978-3-642-15375-4_24.
A. Ehrenfeucht, T. Harju, and G Rozenberg. The Theory of 2-Structures A Framework for Decomposition and Transformation of Graphs. World Scientific, 1999. doi:10.1142/4197.
Uli Fahrenberg, Christian Johansen, Georg Struth, and Ratan Bahadur Thapa. Generating posets beyond n. In Uli Fahrenberg, Peter Jipsen, and Michael Winter, editors, Relational and Algebraic Methods in Computer Science, pages 82–99, Cham, 2020. Springer International Publishing. doi:10.1007/978-3-030-43520-2_6.
Xiang Fu, Tevfik Bultan, and Jianwen Su. Analysis of interacting BPEL web services. In Proceedings of the 13th international conference on World Wide Web, pages 621–630. ACM, 2004. doi:10.1145/988672.988756.
Tibor Gallai. Transitiv orientierbare Graphen. Acta Mathematica Academiae Scientiarum Hungarica, 18(1–2):25–66, 1967.
Jean-Yves Girard. Multiplicatives. In Gabriele Lolli, editor, Logic and Computer Science: New Trends and Applications, pages 11–34. Rosenberg & Sellier, 1987.
Jay L. Gischer. The equational theory of pomsets. Theor. Comput. Sci., 61:199–224, 1988. doi:10.1016/0304-3975(88)90124-7.
Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Computational Logic, 8(1):1–64, 2007. doi:10.1145/1182613.1182614.
Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A proof calculus which reduces syntactic bureaucracy. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of LIPIcs, pages 135–150, Dagstuhl, Germany, 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. doi:10.4230/ LIPIcs.RTA.2010.135.
Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, Computer Science Logic, pages 54–68, Berlin, Heidelberg, 2001. Springer. doi:10.1007/3-540-44802-0_5.
Michel Habib and Christophe Paul. A survey of the algorithmic aspects of modular decomposition. Computer Science Review, 4(1):41–59, 2010. doi:10.1016/j.cosrev.2010.01.001.
Ross Horne. Session subtyping and multiparty compatibility using circular sequents. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1–12:22, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2020.12.
Ross Horne, Sjouke Mauw, and Alwen Tiu. Semantics for specialising attack trees based on linear logic. Fundam. Inform., 153(1-2):57–86, 2017. doi:10.3233/FI-2017-1531.
Ross Horne and Alwen Tiu. Constructing weak simulations from linear implications for processes with private names. Mathematical Structures in Computer Science, 29(8):1275–1308, 2019. doi:10.1017/S0960129518000452.
Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. De Morgan dual nominal quantifiers modelling private names in non-commutative logic. ACM Trans. Comput. Log., 20(4):22:1–22:44, 2019. doi:10.1145/3325821.
Lee O James, Ralph G Stanton, and Donald D Cowan. Graph decomposition for undirected graphs. In Proceedings of the Third Southeastern Conference on Combinatorics, Graph Theory, and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1972), pages 281–290, 1972.
Ozan Kahramanoğulları. System BV is NP-complete. Annals of Pure and Applied Logic, 152(1-3):107–121, 2008. doi:10.1016/j.apal.2007.11.005.
Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, 1978. doi:10.1145/359545.359563.
László Lovász and Michael D Plummer. Matching theory, volume 367. American Mathematical Soc., 2009.
Ross M. McConnell and Jeremy P. Spinrad. Linear-time modular decomposition and efficient transitive orientation of comparability graphs. In Proceedings of the Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA’94, pages 536–545, USA, 1994. Society for Industrial and Applied Mathematics.
Lê Thành D~ ung Nguyê~n and Lutz Straßburger. BV and Pomset Logic are not the same. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1–3:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2022.3.
Mogens Nielsen, Gordon Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13(1):85–108, 1981. Special Issue Semantics of Concurrent Computation. doi:10.1016/0304-3975(81)90112-2.
Vaughan Pratt. Modeling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33–71, 1986. doi:10.1007/BF01379149.
Christian Retoré. Perfect matchings and series-parallel graphs: multiplicative proof nets as R&B-graphs. Electronic Notes in Theoretical Computer Science, 3, 1996. doi:10.1016/ S1571-0661(05)80416-5.
Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, pages 300–318, Berlin, Heidelberg, 1997. Springer. doi:10.1007/3-540-62688-3_43.
Christian Retoré. Handsome proof-nets: perfect matchings and cographs. Theoretical Computer Science, 294(3):473–488, 2003. doi:10.1016/S0304-3975(01)00175-X.
Lutz Straßburger. Linear Logic and Noncommutativity in the Calculus of Structures. PhD thesis, Technische Universität Dresden, 2003.
Jacobo Valdes, Robert E Tarjan, and Eugene L Lawler. The recognition of series parallel digraphs. In Proceedings of the eleventh annual ACM symposium on Theory of computing, pages 1–12. ACM, 1979. doi:10.1137/0211023.