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
We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.
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
We consider networks of weighted processes that consist of an arbitrary number of weighted automata equipped with weights taken from a monoid. We investigate parameterized model checking problems used to verify whether certain qualitative and quantitative properties hold independently of the number of processes. We prove that model checking properties expressed in a weighted extension of LTL is decidable if the monoid satisfies some simple properties. We further present decision procedures for checking global properties of weighted networks.
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
During the last years, weighted timed automata have received much interest in the real-time community. Weighted timed automata form an extension of timed automata and allow us to assign weights (costs) to both locations and edges. This model, introduced by Alur et al. (2001) and Behrmann et al. (2001), permits the treatment of continuous consumption of resources and has led to much research on scheduling problems, optimal reachability and model checking. Also, several authors have derived Kleene-type characterizations of (unweighted) timed automata and their accepted timed languages. The goal of this paper is to provide a characterization of the behaviours of weighted timed automata by rational power series. We define weighted timed automata with weights taken in an arbitrary semiring, resulting in a model that subsumes several weighted timed automata concepts of the literature. For our main result, we combine the methods of Schützenberger, a recent approach for a Kleene-type theorem for unweighted timed automata by Bouyer and Petit as well as new techniques. Our main result also implies Kleene-type theorems for several subclasses of weighted timed automata investigated before, e. g. , for timed automata and timed automata with stopwatch observers.