BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260408T233845Z
UID:Seminar-verification-1330@lxserverA.csc.liv.ac.uk.csc.liv.ac.uk
ORGANIZER:CN=Patrick Totzke:MAILTO:totzke@liverpool.ac.uk
DTSTART:20260219T110000
DTEND:20260219T120000
SUMMARY:Verification Series
DESCRIPTION:David Purser: Automata Automata\n\nWe study verification problems for history-constrained systems (HCS), a model of guarded computation that uses nested systems. An outer system describes the process architecture in which a sequence of actions represents the communication between sub-systems through a global bus. Actions are either permitted or blocked locally by guards; these guards read and decide based on the sequence of actions so far in the global bus.  \n\n\n\nWhen HCS have both the outer systems and the local guard controllers modelled by finite automata, we show they have the same expressive power as regular languages and finite automata, but they are exponentially more succinct. We also analyse games on this model, representing the interaction between environment and controller, and show that solving such games is EXPTIME-complete, where the lower bound already holds for reachability/safety games and the upper bound holds for any ω-regular winning condition. Finally, we consider HCS with guards of greater expressive power, Vector Addition Systems with States (VASS). We show that with deterministic coverability-VASS guards the reachability problem is EXPSPACE-complete, while with reachability-VASS the problem is undecidable.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=1330
LOCATION:Ashton 208
END:VEVENT
END:VCALENDAR