Skip to Main content Skip to Navigation

Expressive Equivalence and Succinctness of Parametrized Automata with respect to Finite Memory Automata

Tushant Jha 1 Walid Belkhir 2, 1 Yannick Chevalier 3, * Michael Rusinowitch 1
* Corresponding author
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We compare parametrized automata, a class of automata recently introduced by the authors, against finite memory automata with non-deterministic assignment, an existing class of automata used to model services. We prove that both classes have the same expressive power, while parametrized automata can be exponentially succinct in some cases. We then prove that deciding simulation preorder for parametrized automata is EXPTIME-complete, extending an earlier result showing it in EXPTIME.
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-01224144
Contributor : Walid Belkhir <>
Submitted on : Wednesday, November 4, 2015 - 10:49:04 AM
Last modification on : Thursday, March 26, 2020 - 5:07:53 PM
Document(s) archivé(s) le : Friday, February 5, 2016 - 10:35:57 AM

File

FOR-MOVES_2015_paper_1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01224144, version 1

Citation

Tushant Jha, Walid Belkhir, Yannick Chevalier, Michael Rusinowitch. Expressive Equivalence and Succinctness of Parametrized Automata with respect to Finite Memory Automata. FOR-MOVES 2015: FORmal MOdeling and VErification of Service-based systems, Nov 2015, Goa, India. ⟨hal-01224144⟩

Share

Metrics

Record views

631

Files downloads

1038