Algorithmics on Infinite State Systems 2012

(AISS 2012)

A satellite workshop of LICS 2012

June 29th, Dubrovnik (Croatia)


The workshop provides the opportunity to assess recent scientific advances and exchange ideas on the algorithmic theory of infinite state systems. Infinite state systems arise in many areas of computer science. Typical examples are recursive programs, communicating systems with unbounded buffers and real time systems. Important algorithmic techniques dealing with infinite state systems include model checking, reachability and equivalence checking.

There are two main goals of the workshop:

- Bringing together leading experts as well as young scientists interested in foundational research on infinite state systems in order to exchange their ideas.

- Presenting the latest developments in the area of infinite state systems to a wider audience interested in computer science logic.


AISS12 is a satellite workshop of LICS 2012, and will be held on Friday, June 29, 2012. Presentations are selected on the basis of an abstract of up to 4 pages (including references) describing the research. The format is not particularly specified. Submissions are judged on the expected interest in and quality of the planned talk. The accepted abstracts will be made available at the workshop, but no formal proceedings are planned. It is thus also allowed (and encouraged) to send recent results that have been published at other conferences (although preferably neither at LICS 2012 nor any of its other satellite workshops).


4-page abstracts should be submitted via the AISS submission page on the EasyChair system.


Topics include but are not restricted to (no order):

- abstract machine models for infinite state systems (e.g. pushdown systems, higher-order pushdown systems, one-counter machines)

- Petri nets

- automatic structures

- well-structured transition systems

- rewriting formalisms for infinite state systems (e.g. ground tree rewriting)

- higher-order recursion schemes

- algorithmic model theory

- games on infinite arenas

- model checking for infinite state systems (e.g. model checking for MSO, FO, CTL, LTL, mu-calculus)

- equivalence checking of infinite state systems, (e.g. bisimilarity checking)

- decomposition techniques for infinite state systems (e.g. Feferman/Vaught decompositions)

- reachability in infinite state systems




Author of picture: Gari Baldi, copyright cc-by-sa-2.0