Author name cluster
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.
Highlights Conference 2024 Conference Abstract
We define Büchi automata over concrete domains, where transitions are labelled with constraints. We then give an overview over the decidability status of the nonemptiness problem for such automata over typical concrete domains, and we explain the symbolic approach as a tool to prove decidability of the nonemptiness problem.
JELIA Conference 2023 Conference Paper
Abstract We consider the description logic \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}^{\mathcal {P}}(\mathcal {D}_{\varSigma })\) over the concrete domain \(\mathcal {D}_{\varSigma } = (\varSigma ^*, \prec, =, (=_{\mathfrak {w}})_{\mathfrak {w}\in \varSigma ^*})\), where \(\prec \) is the strict prefix order over finite strings in \(\varSigma ^*\). Using an automata-based approach, we show that the concept satisfiability problem w. r. t. general TBoxes for \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}^{\mathcal {P}}(\mathcal {D}_{\varSigma })\) is ExpTime -complete for all finite alphabets \(\varSigma \). As far as we know, this is the first complexity result for an expressive description logic with a nontrivial concrete domain on strings.
MFCS Conference 2022 Conference Paper
We study constraint automata that accept data languages on finite string values. Each transition of the automaton is labelled with a constraint restricting the string value at the current and the next position of the data word in terms of the prefix and the suffix order. We prove that the emptiness problem for such constraint automata with Büchi acceptance condition is NL-complete. We remark that since the constraints are formed by two partial orders, prefix and suffix, we cannot exploit existing techniques for similar formalisms. Our decision procedure relies on a decidable characterization for those infinite paths in the graph underlying the automaton that can be completed with string values to yield a Büchi-accepting run. Our result is - to the best of our knowledge - the first work in this context that considers both prefix and suffix, and it is a first step into answering an open question posed by Demri and Deters.
TCS Journal 2020 Journal Article
Highlights Conference 2018 Conference Abstract
ABSTRACT. We study the containment problem for unambiguous register automata. Register automata, introduced by Kaminski and Francez in 1994, extend finite automata with a finite set of registers. Register automata can process data words, i. e. , finite words over an infinite data domain; the registers are used to store data coming from the input word for later comparisons. A register automaton is unambiguous if it has at most one accepting run for every input data word. We prove that the class of languages recognized by these automata is not closed under complement, thereby preventing a classical reduction of the containment problem to the emptiness problem for register automata. We nonetheless prove that the containment problem for unambiguous register automata is decidable, based on a reduction to a reachability problem on some finite graph. (This is joint work with Antoine Mottet.)
MFCS Conference 2016 Conference Paper
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.
Highlights Conference 2016 Conference Abstract
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.
Highlights Conference 2015 Conference Abstract
We study decidability of verication problems for timed automata extended with a pushdown stack or discrete counters. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this work is to investigate the language inclusion problem and related problems for this class of automata and over finite timed words. On the negative side, we prove that the language inclusion problem is undecidable for the case that A is a pushdown timed automaton and B is a one-clock timed automaton. This is even the case if A is a deterministic instance of a very restricted subclass of timed pushdown automata called timed visibly one-counter nets. On the positive side, we prove that the language inclusion problem is decidable if A is a timed automaton and B is a timed automaton extended with a finite set of counters that can be incremented and decremented, and which we call timed counter nets. As a special case, we obtain the decidability of the universality problem for timed counter nets: given a timed automaton A with input alphabet $\Sigma$, does L(A) accept the set of all timed words over $\Sigma$? Finally, we give the precise decidability border for the universality problem by proving that the universality problem is undecidable for the class of timed visibly one-counter automata.
TCS Journal 2014 Journal Article
Highlights Conference 2013 Conference Abstract
We consider TPTL(Z) and MTL(Z) whose semantics are based on nonmonotonic data words in which every point is assigned a natural number as its weight. We define a weighted version of the EF game on MTL. Using these games, we prove the following: 1. TPTL(Z) is strictly more expressive than MTL(Z). 2. The until hierarchy and the constant hierarchy are strict for MTL(Z). 3. It is undecidable whether a given TPTL(Z) formula can be expressed in MTL(Z).
TCS Journal 2011 Journal Article