8 papers
Learning Canonical Register Automata over Ordered Data Domains
Yong Li, Qiyi Tang, Di-De Yen
Register automata are finite automata equipped with memory that recognize data languages over infinite alphabets. In this work, we investigate active learning algorithms for determ…
Optimal LTLf Synthesis
Yujian Cao, Sven Schewe, Qiyi Tang +1
Strategy synthesis typically follows an all-or-nothing paradigm, returning unrealisable whenever a specification cannot be guaranteed in an uncertain environment. In this paper, we…
Hyper-Minimization for Deterministic Register Automata
Yong Li, Qiyi Tang, Di-De Yen
We investigate hyper-minimization for deterministic register automata (DRAs). We begin by introducing DRA counterparts of classical notions from deterministic finite automata. Buil…
The Complexity of Games with Randomised Control
Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul +5
We study the complexity of solving two-player infinite duration games played on a fixed finite graph, where the control of a node is not predetermined but rather assigned randomly.…
Good-for-MDP State Reduction for Stochastic LTL Planning
Christoph Weinhuber, Giuseppe De Giacomo, Yong Li +2
We study stochastic planning problems in Markov Decision Processes (MDPs) with goals specified in Linear Temporal Logic (LTL). The state-of-the-art approach transforms LTL formulas…
Efficient Learning of Weak Deterministic Büchi Automata
Mona Alluwayma, Yong Li, Sven Schewe +1
We present an efficient Angluin-style learning algorithm for weak deterministic Büchi automata (wDBAs). Different to ordinary deterministic Büchi and co-Büchi automata, wDBAs have…
Resolving Nondeterminism by Chance
Soumyajit Paul, David Purser, Sven Schewe +3
History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next…
Minimising the Probabilistic Bisimilarity Distance
Stefan Kiefer, Qiyi Tang
A labelled Markov decision process (MDP) is a labelled Markov chain with nondeterminism; i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is…