Cryptology ePrint Archive: Report 2021/798

Probabilistic Dynamic Input Output Automata

Pierre Civit and Maria Potop-Butucaru

Abstract: We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism [1] to 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 to probabilistic settings all these features. Furthermore, we prove necessary and sufficient conditions to obtain the implementation monotonicity with respect to automata creation and destruction. Our work lays down the premises for extending composable secure-emulation [3] 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).

Category / Keywords: foundations / I/O automata, dynamic systems, probabilistic systems, modelisation

Date: received 11 Jun 2021

Contact author: pierrecivit at gmail com, maria potop-butucaru at lip6 fr

Available format(s): PDF | BibTeX Citation

Version: 20210614:134842 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]