Mahsa Shirmohammadi

Highlights Conference 2025 Conference Abstract

Differential Tree Automata

• Mahsa Shirmohammadi

CSL Conference 2025 Conference Paper

Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

• Andrew Scoones
• Mahsa Shirmohammadi
• James Worrell 0001

Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are read-once variables: they do not affect the control flow of the automaton and their value is output only at the end of a run. Thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution - a result of independent interest - is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.

I&C Journal 2022 Journal Article

Costs and rewards in priced timed automata

• Martin Fränzle
• Mahsa Shirmohammadi
• Mani Swaminathan
• James Worrell

We consider Pareto analysis of multi-priced timed automata (MPTA) having multiple observers recording costs (to be minimised) and rewards (to be maximised) along a computation. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location such that the accumulated costs and rewards Pareto dominate a given vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. We show the problem to be PSPACE-complete for MPTA recording only costs or only rewards. We also consider an approximate Pareto Domination that is decidable in exponential time with no restrictions on types and number of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers entails translation to a decidable fragment of arithmetic involving quadratic forms.

Highlights Conference 2018 Conference Abstract

Costs and Rewards in Priced Timed Automata

• Mahsa Shirmohammadi

ABSTRACT. We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms. The talk is on a paper that is going to be presented in ICALP 2018.

SODA Conference 2017 Conference Paper

On Rationality of Nonnegative Matrix Factorization

• Dmitry Chistikov 0001
• Stefan Kiefer
• Ines Marusic
• Mahsa Shirmohammadi
• James Worrell 0001

Nonnegative matrix factorization ( N MF) is the problem of decomposing a given nonnegative n × m matrix M into a product of a nonnegative n × d matrix W and a nonnegative d × m matrix H. NMF has a wide variety of applications, including bioinformatics, chemometrics, communication complexity, machine learning, polyhedral combinatorics, among many others. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether every rational matrix M has an NMF with minimal d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix M for which W and H require irrational entries. As an application of this result, we show that state minimization of labeled Markov chains can require the introduction of irrational transition probabilities. We complement these irrationality results with an NP- complete version of NMF for which rational numbers suffice.

Highlights Conference 2016 Conference Abstract

Minimal probabilistic automata have to make irrational choices

• Mahsa Shirmohammadi
• Dmitry Chistikov
• Stefan Kiefer
• Ines Marusic
• James Worrell

In this talk, we answer the question of whether, given a probabilistic automaton (PA) with rational transition probabilities, there always exists a minimal equivalent PA that also has rational transition probabilities. The PA and its minimal equivalent PA accept all finite words with equal probabilities. We approach this problem by exhibiting a connection with a longstanding open question concerning nonnegative matrix factorization (NMF). NMF is the problem of decomposing a given nonnegative n*m matrix M into a product of a nonnegative n*d matrix W and a nonnegative d*m matrix H. In 1993 Cohen and Rothblum posed the problem of whether a rational matrix M always has an NMF of minimal inner dimension d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix for which W and H require irrational entries. As a corollary we obtain a negative answer to the question on rationality of minimal probabilistic automata. This talk is based on the paper titled “On Restricted Nonnegative Matrix Factorization”, that will be presented in ICALP 2016, and the unpublished manuscript titled “Nonnegative Matrix Factorization Requires Irrationality”, that is now online on Arxiv (https: //arxiv. org/abs/1605. 06848v1).

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.

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.

Highlights Conference 2013 Conference Abstract

Synchronization in Markov decision processes

• Mahsa Shirmohammadi
• Laurent Doyen
• Thierry Massart

Markov Decision Processes (MDPs) are 1-1/2 player stochastic games. The player tries to maximize the probability to satisfy an objective. Traditionally, the objective of the player is expressed as a set of desired sequences of states visited during the game. Recently, MDPs are viewed as generators of probability distributions over states, and objectives are defined as sets of sequences of probability distributions. We study synchronizing objectives that require that some state tend to accumulate all the probability mass. We consider three winning modes: sure, almost-sure and limit-sure.

MFCS Conference 2011 Conference Paper

Infinite Synchronizing Words for Probabilistic Automata

• Laurent Doyen 0001
• Thierry Massart
• Mahsa Shirmohammadi

Abstract Probabilistic automata are finite-state automata where the transitions are chosen according to fixed probability distributions. We consider a semantics where on an input word the automaton produces a sequence of probability distributions over states. An infinite word is accepted if the produced sequence is synchronizing, i. e. the sequence of the highest probability in the distributions tends to 1. We show that this semantics generalizes the classical notion of synchronizing words for deterministic automata. We consider the emptiness problem, which asks whether some word is accepted by a given probabilistic automaton, and the universality problem, which asks whether all words are accepted. We provide reductions to establish the PSPACE-completeness of the two problems.