Document Open Access Logo

Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications

Authors Ashwin Bhaskar , M. Praveen

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.14.pdf
  • Filesize: 0.91 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
Keywords
  • Distributed Systems
  • Interface Automata
  • Registers
  • Parity Games

Metrics

Abstract

When multiple software components interact via method calls, we may want to ensure that the order of invoked methods and the arguments provided adhere to some specification. The classic problem associated with interface automata checks for the existence of a mediator whose intention is to act as a buffer in between method invocations so that invocations do not go unanswered. We extend the base model underlying interface automata, enabling them to exchange integer values - one automaton generates an integer value and outputs it by firing a generating transition and another automaton receives the value by synchronously firing a receiving transition. Transitions in the automata can have guards with linear order constraints on the exchanged values, influencing which methods can or can not be invoked later. So the generated values influence the sequences of invocations that are enabled. We specify desirable properties of the sequence of method calls and the arguments passed to them using an extension of Linear Temporal Logic (LTL). We consider the interoperability problem, which is to check if it is possible to generate integer values in such a way that all enabled sequences satisfy the given specification. 
We show that the interoperability problem is undecidable in general, even when there are only two participating automata. We show decidability in the case where guards on generating transitions can only have equality constraints on the exchanged value (but receiving transitions can continue to have linear order constraints). We model this problem as a game between two players, one trying to generate integer values such that violating sequences are disabled while the other player tries to dig out violating sequences that are enabled. Interoperability is equivalent to the first player having a winning strategy. We solve this game via a finite abstraction, which results in a symbolic game. We then show that winning strategies for the symbolic game can be translated to winning strategies for the original game over integers.

Cite As Get BibTex

Ashwin Bhaskar and M. Praveen. Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.14

Author Details

Ashwin Bhaskar
  • Chennai Mathematical Institute, India
M. Praveen
  • Chennai Mathematical Institute, India
  • CNRS IRL ReLaX, Chennai, India

Funding

  • Praveen, M.: This author is partially supported by the Infosys foundation.

References

  1. Sarra Alqahtani, Xinchi He, Rose Gamble, and Mauricio Papa. Formal verification of functional requirements for smart contract compositions in supply chain management systems. In Proceedings of the 53rd Hawaii International Conference on System Sciences, 2020. URL: https://doi.org/10.24251/HICSS.2020.650.
  2. Ashwin Bhaskar and M Praveen. Constraint ltl with remote access. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023), pages 41:1-41:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2023.41.
  3. Ashwin Bhaskar and M Praveen. Realizability problem for constraint ltl. Information and Computation, 296:105126, 2024. URL: https://doi.org/10.1016/J.IC.2023.105126.
  4. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theoretical Computer Science, 458:49-60, 2012. URL: https://doi.org/10.1016/J.TCS.2012.07.038.
  5. Luca De Alfaro and Thomas A Henzinger. Interface automata. ACM SIGSOFT Software Engineering Notes, 26(5):109-120, 2001. URL: https://doi.org/10.1145/503209.503226.
  6. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk. Energy and mean-payoff games with imperfect information. In International Workshop on Computer Science Logic, pages 260-274. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_22.
  7. Stéphane Demri and Deepak D’Souza. An automata-theoretic approach to constraint LTL. Information and Computation, 205(3):380-415, 2007. URL: https://doi.org/10.1016/j.ic.2006.09.006.
  8. Léo Exibard, Emmanuel Filiot, and Ayrat Khalimov. Church synthesis on register automata over linearly ordered data domains. Formal Methods in System Design, 61(2):290-337, 2022. URL: https://doi.org/10.1007/S10703-023-00435-W.
  9. Erich Gradel and Wolfgang Thomas. Automata, logics, and infinite games: a guide to current research, volume 2500. Springer Science & Business Media, 2002. Google Scholar
  10. Lukáš Holík, Malte Isberner, and Bengt Jonsson. Mediator synthesis in a component algebra with data. In Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings, pages 238-259. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23506-6_16.
  11. Gabor Madl, Luis Bathen, German Flores, and Divyesh Jadav. Formal verification of smart contracts using interface automata. In 2019 IEEE International Conference on Blockchain (Blockchain), pages 556-563. IEEE, 2019. Google Scholar
  12. Marvin L Minsky. Recursive unsolvability of post’s problem of" tag" and other topics in theory of turing machines. Annals of Mathematics, 74(3):437-455, 1961. Google Scholar
  13. Nir Piterman. From nondeterministic büchi and streett automata to deterministic parity automata. Logical Methods in Computer Science, 3, 2007. URL: https://doi.org/10.2168/LMCS-3(3:5)2007.
  14. Ayleen Schinko, Walter Vogler, Johannes Gareis, N Tri Nguyen, and Gerald Lüttgen. Interface automata for shared memory. Acta Informatica, 59(5):521-556, 2022. URL: https://doi.org/10.1007/S00236-021-00408-8.
  15. Moshe Y Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331. IEEE Computer Society, 1986. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact