Author name cluster

Parvaneh Babari

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

TCS Journal 2018 Journal Article

Weighted register automata and weighted logic on data words

Parvaneh Babari
Manfred Droste
Vitaly Perevoshchikov

Data words are sequences of pairs where the first element is taken from a finite alphabet and the second element is taken from an infinite data domain. Register automata provide a widely studied model for reasoning on data words. In this paper, we investigate automata models for quantitative aspects of systems with infinite data domains, e. g. , the costs of storing data on a remote server or the consumption of resources (e. g. , memory, energy, time) during a data analysis. We introduce weighted register automata on data words over commutative data semirings equipped with a collection of binary data functions, and we investigate their closure properties. Unlike the other models considered in the literature, we allow data comparison by means of an arbitrary collection of binary data relations. This enables us to incorporate timed automata and weighted timed automata into our framework. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic; for the proof we employ a new class of determinizable visibly register automata.

Details DOI

MFCS Conference 2016 Conference Paper

Synchronizing Data Words for Register Automata

Parvaneh Babari
Karin Quaas
Mahsa Shirmohammadi

Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is co-NEXPTIME-complete.

Details

Highlights Conference 2016 Conference Abstract

Synchronizing Data Words for Register Automata

Karin Quaas
Parvaneh Babari
Mahsa Shirmohammadi

Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with only 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and it is in NLOGSPACE for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is coNEXTPTIME-complete. This is joint work with Parvaneh Babari (University of Leipzig) and Mahsa Shirmohammadi (University of Oxford), accepted at MFCS 2016.

Details

Highlights Conference 2015 Conference Abstract

Weighted Register Automata and Weighted Existential MSO Logic on Data Words

Parvaneh Babari

In these paper, we deal with the automata models for quantitative aspects of systems with infinite data domains, e. g. , the costs of storing data on a remote server or the consumption of resources (e. g. , memory, energy, time) during a data analysis. We introduce weighted register automata on data words, study their closure properties and introduce a determinizable subclass of them. In our main result, we give a logical characterization of weighted register automata by means of weighted existential monadic second-order logic.

Details