Document Open Access Logo

Dynamic Probabilistic Input Output Automata

Authors Pierre Civit, Maria Potop-Butucaru

PDF

File

Thumbnail PDF
PDF
LIPIcs.DISC.2022.15.pdf
  • Filesize: 1.08 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
Keywords
  • Automata
  • Distributed Computing
  • Formal Verification
  • Dynamic systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism of Attie & Lynch [Paul C. Attie and Nancy A. Lynch, 2016] to the probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion. They can model mobility by using signature modification. They are also hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton. Our work extends all these features to the probabilistic setting. Furthermore, we prove necessary and sufficient conditions to obtain the monotonicity of automata creation/destruction with implementation preorder. Our construction uses a novel proof technique based on homomorphism that can be of independent interest. Our work lays down the foundations for extending composable secure-emulation of Canetti et al. [Ran Canetti et al., 2007] to dynamic settings, an important tool towards the formal verification of protocols combining probabilistic distributed systems and cryptography in dynamic settings (e.g. blockchains, secure distributed computation, cybersecure distributed protocols, etc).

Cite As Get BibTex

Pierre Civit and Maria Potop-Butucaru. Dynamic Probabilistic Input Output Automata. In 36th International Symposium on Distributed Computing (DISC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 246, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.DISC.2022.15

Author Details

Pierre Civit
  • Sorbonne Université, CNRS, LIP6, Paris, France
Maria Potop-Butucaru
  • Sorbonne Université, CNRS, LIP6, Paris, France

References

  1. Edward A. Ashcroft. Proving assertions about parallel programs. J. Comput. Syst. Sci., 10(1):110-135, 1975. URL: https://doi.org/10.1016/S0022-0000(75)80018-3.
  2. Paul C. Attie and Nancy A. Lynch. Dynamic input/output automata: A formal and compositional model for dynamic systems. Inf. Comput., 249:28-75, 2016. URL: https://doi.org/10.1016/j.ic.2016.03.008.
  3. Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala. Task-Structured Probabilistic I/O Automata. Journal of Computer and System Sciences, 94:63 - -97, 2018. URL: https://doi.org/10.1016/j.jcss.2017.09.007.
  4. Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Moses D. Liskov, Nancy A. Lynch, Olivier Pereira, and Roberto Segala. Using probabilistic I/O automata to analyze an oblivious transfer protocol. IACR Cryptol. ePrint Arch., page 452, 2005. URL: http://eprint.iacr.org/2005/452.
  5. Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Nancy A. Lynch, and Olivier Pereira. Compositional security for task-pioas. In 20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy, pages 125-139. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/CSF.2007.15.
  6. Jing Chen and Silvio Micali. Algorand: A secure and efficient distributed ledger. Theor. Comput. Sci., 777:155-183, 2019. URL: https://doi.org/10.1016/j.tcs.2019.02.001.
  7. Pierre Civit and Maria Potop-Butucaru. Probabilistic dynamic input output automata (extended version). Cryptology ePrint Archive, Paper 2021/798, 2021. URL: https://doi.org/10.4230/LIPIcs.DISC.2022.20.
  8. Pierre Civit and Maria Potop-Butucaru. Brief announcement: Composable dynamic secure emulation. In Kunal Agrawal and I-Ting Angelina Lee, editors, SPAA '22: 34th ACM Symposium on Parallelism in Algorithms and Architectures, Philadelphia, PA, USA, July 11 - 14, 2022, pages 103-105. ACM, 2022. URL: https://doi.org/10.1145/3490148.3538562.
  9. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  10. Richard M. Karp and Raymond E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  11. Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng., 3(2):125-143, 1977. URL: https://doi.org/10.1109/TSE.1977.229904.
  12. Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. A theory of atomic transactions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 326 LNCS:41-71, 1988. URL: https://doi.org/10.1007/3-540-50171-1_3.
  13. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  14. Rocco De Nicola and Roberto Segala. A process algebraic view of input/output automata. Theor. Comput. Sci., 138(2):391-423, 1995. URL: https://doi.org/10.1016/0304-3975(95)92307-J.
  15. Susan S. Owicki and David Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319-340, 1976. URL: https://doi.org/10.1007/BF00268134.
  16. C.A. Petri. Kommunikation mit Automaten. PhD thesis, Institut für instrumentelle Mathematik, Bonn, 1962. Google Scholar
  17. Martin L. Puterman. Markov decision processes: discrete stochastic dynamic programming. Wiley series in probability and mathematical statistics. John Wiley & Sons, 1 edition, 1994. Google Scholar
  18. Alejandro Ranchal-Pedrosa and Vincent Gramoli. Platypus: Offchain protocol without synchrony. In Aris Gkoulalas-Divanis, Mirco Marchetti, and Dimiter R. Avresky, editors, 18th IEEE International Symposium on Network Computing and Applications, NCA 2019, Cambridge, MA, USA, September 26-28, 2019, pages 1-8. IEEE, 2019. URL: https://doi.org/10.1109/NCA.2019.8935037.
  19. Roberto Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusettes Institute of technology, 1995. Google Scholar
  20. Frits W. Vaandrager. On the relationship between process algebra and input/output automata. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 387-398. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151662.
  21. Kazuki Yoneyama. Formal modeling of random oracle programmability and verification of signature unforgeability using task-pioas. Int. J. Inf. Sec., 17(1):43-66, 2018. URL: https://doi.org/10.1007/s10207-016-0352-y.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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