INFINITY 2023

23rd International Workshop on Verification of Infinite-State Systems

, Antwerp, Belgium
Co-located with CONFEST and CONCUR 2023, the 34th International Conference on Concurrency Theory.
Aim:

The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of mathematical techniques for the analysis and verification of systems with infinitely many states. The plan is to discuss recent results, emerging research directions, promising applications, open problems and stimulate cooperation among researchers working in the field of counter systems.

Topics:

Topics of interest include (but are not limited to):

  • Vector Addition Systems aka Petri nets
  • Counter and pushdown systems
  • Probabilistic and timed systems
  • Parameterised systems
  • Infinite-state models of software/hardware systems
  • Model-checking, reachability problems, static analysis, symbolic analysis, abstraction techniques, abstract interpretation, preorder/equivalence-checking, and control synthesis for infinite-state systems.

Call for Presentations

We invite contributed talks of around 20 minutes (exact duration TBC). The talk should be based on recent results, current progress, emerging research directions, promising applications, work in progress, failure reports and open problems etc (the work does not need to be published).

Please email both organisers to propose a talk, preferably before 15th August 2023. The email should contain a title, short abstract (2-3 paragraphs) and a link to a related paper (if there is one). We will notify acceptance within 1 week of your email.

There are no formal proceedings.

Program

Location: 1st Floor, Prentenkabinet

The programme will consist of invited talks, contributed talks by workshop participants and an open problem discussion.

Invited Speakers:
  • Patrick Totzke, Liverpool, UK.
    History determinism for infinite-state systems

    History determinism sits between deterministic and non-deterministic models, requiring that non-determinism can be resolved on-the-fly, that is, without knowledge of the future. Whilst there has been much work on history determinism for finite-state models, this talk will focus on recent advancements in the study of history determinism for infinite-state models, including timed automata and vector addition systems.

  • Lorenzo Clemente, University of Warsaw, Poland.
    The equality problem in automata, combinatorics, and logic

    We survey decidability and complexity of the equality problem for number sequences and power series arising in automata theory, enumerative combinatorics, and logic. For automata and combinatorics, we show old and new results about deciding equality for constructible algebraic, D-finite, and constructible differentially algebraic power series. For logic, natural number sequences arise from 1) model counting for first-order logic and 2) orbit counting for the action of oligomorphic permutation groups, however this second part will mostly be about open problems.

  • Rupak Majumdar, MPI-SWS, Kaiserslautern, Germany.
    Sequential Decision Making with Incomplete Information and Communication

    Unfortunately Rupak had to cancel.

Accepted Contributed Talks and Programme:
Time Event Title
9:00 - 10:00 Patrick Totzke
Invited Speaker 		History determinism for infinite-state systems
10:00 - 10:25 Coffee break
10:25 - 10:50 Roland Guttenberg Geometry of Vector Addition Systems: Hole-Freedom
10:50 - 11:15 Tim Leys The Geometry of Reachability sets in Continuous VASS
11:15 - 11:30 Mini-break (no coffee)
11:30 - 11:55 Filip Mazowiecki Fun with VASS
11:55 - 12:20 Qiyi Tang On the Succinctness of Good-for-MDPs Automata
12:20 - 13:45 Lunch
13:45 - 14:45 Lorenzo Clemente
Invited Speaker		 The equality problem in automata, combinatorics, and logic
14:45 - 14:55 Mini-break (no coffee)
14:55 - 15:20 Arka Ghosh Hilbert's basis for polynomial rings with infinitely many variables
15:20 - 15:45 Toghrul Karimov Abstraction-based verification of linear dynamical systems
15:45 - 16:10 Coffee break
16:10 - 16:35 Joshua Jeppson STAMINA tool for infinite-state probabilistic systems
16:35 - 17:30 Open problem session
All workshop participants (speaker or not) are invited to bring an open problem and be prepared to present it (using up to 5 minutes). Please let the organisers know during the breaks on the day.
18:00 onwards CONFEST Opening reception
Entrance hall & terrace Building R

Organisation

Infinity 2023 is organised by David Purser and Filip Mazowiecki as part of CONFEST 2023.

Contact: and f.mazowiecki[obvious-symbol]uw.edu.pl.

Infinity 2023 takes place in person as a workshop at CONFEST 2023 in Antwerp, Belgium. See the CONFEST website for location and venue details.

Registration

Registration is handled by CONFEST and is open. Please register here https://www.uantwerpen.be/en/conferences/confest-2023/registration/, being sure to indicate participation in the pre-conference workshops (RADICAL, EXPRESS/SOS, INFINITY) on September 18. Note it is slightly cheaper if you register by August 6th.

Past Events