IMDEA Software
María de Maeztu

IMDEA initiative

Home > Events > Invited Talks > 2025 > Live long enough to see them die: observing mortality of labelled transition systems

Thursday, September 4, 2025

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)

Andrew Ryzhikov, Postdoctoral Researcher, MIMUW, University of Warsaw

Live long enough to see them die: observing mortality of labelled transition systems

Abstract:

A labelled transition system is a directed graph whose edges are labelled with letters from a finite alphabet. The vertices of the digraph are the states of the system, and, for an input letter, the system nondeterministically choses an outgoing edge labelled by this letter and moves to the next state according to it. If there are no such outgoing edges, the system “dies”, that is, moves to an unsafe state. We consider the setting where we know the structure of a labelled transition system and the sequence of input letters, but we don’t know the current state of the system and the nondeterministic choices it makes. We study sequences of letters that guarantee entering the unsafe state regardless of the current state of the system and the choices it makes. Such sequences are called mortal. I will discuss the following questions: what is the computational complexity of deciding if a mortal sequence exists? for a given number of states, what is the maximum length of a shortest mortal sequence? The latter question can be interpreted as follows: what is the lower bound on the time that we need to spend observing a system before we know that it has entered the unsafe state? I will describe two equivalent ways of talking about such systems: via nondeterministic finite automata and via sets of nonnegative matrices. I will also explain our recent results with Stefan Kiefer (University of Oxford) about a subclass of labelled transition systems where many similar properties can be efficiently decided.