Energy games and multiweighted modal automata
Title: Energy games and multiweighted modal automata
Speaker: Dr. Line Juhl
Time: 14:00-15:00, Tuesday, July 3rd, 2012
Venue: Lecture Room 337.
Abstract:
I will present two lines of research that both incorporate game theoretical aspects. The first part is on energy games that are games played on finite weighted automata and concern the existence of infinite runs subject to boundary constraints on the accumulated weight, allowing e.g. only for behaviours where a resource is always available (nonnegative accumulated weight), yet does not exceed a given maximum capacity. We extend energy games to a multiweighted and parameterized setting, allowing us to model systems with multiple quantitative aspects. By several different reductions new complexity and (un)decidability results for both one- and two-player games are identified.
I will present two lines of research that both incorporate game theoretical aspects. The first part is on energy games that are games played on finite weighted automata and concern the existence of infinite runs subject to boundary constraints on the accumulated weight, allowing e.g. only for behaviours where a resource is always available (nonnegative accumulated weight), yet does not exceed a given maximum capacity. We extend energy games to a multiweighted and parameterized setting, allowing us to model systems with multiple quantitative aspects. By several different reductions new complexity and (un)decidability results for both one- and two-player games are identified.
Furthermore we see how games can be used in connection with modal transition systems. Multiweighted modal automata provide a specification theory for multiweighted transition systems. We propose a simple fragment of CTL that is able to express properties about accumulated weights along maximal runs of multiweighted modal automata. Our logic is equipped with a game-based semantics and guarantees both soundness (formula satisfaction is propagated to the modal refinements) as well as completeness (formula non-satisfaction is propagated to at least one of its implementations).