23rd International Workshop on Verification of Infinite-State Systems
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 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.
Location: 1st Floor, Prentenkabinet
The programme will consist of invited talks, contributed talks by workshop participants and an open problem discussion.
- 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:
|9:00 - 10:00||Patrick Totzke
|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
|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
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 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.
- Infinity 2023, Antwerp, Belgium with CONCUR
- Infinity 2020, Online with LICS and ICALP
- Infinity 2019, Taipei, Taiwan with ATVA
- Infinity 2018, Prague, Czech Republic with ICALP
- Infinity 2017, Reykjavik, Iceland with LICS
- Infinity 2016, Singapore, Singapore with Automata, Logic and Games 2016
- Infinity 2015, Bangalore, India with FSTTCS
- Infinity 2014, New Delhi, India with FSTTCS
- Infinity 2013, Hanoi, Vietnam with ATVA
- Infinity 2012, Paris, France with FM
- Infinity 2011, Taipei, Taiwan with ATVA
- Infinity 2010, Singapore, Singapore with ATVA
- Infinity 2009, Bologna, Italy with CONCUR
- Infinity 2008, Toronto, Canada with CONCUR
- Infinity 2007, Lisbon, Portugal with CONCUR
- Infinity 2006, Bonn, Germany with CONCUR
- Infinity 2005, San Francisco, USA with CONCUR
- Infinity 2004, London, UK with CONCUR
- Infinity 2003, Marseilles, France with CONCUR
- Infinity 2002, Brno, Czech Republic with CONCUR
- Infinity 1998, Aalborg, Denmark with ICALP
- Infinity 1997, Bologna, Italy with ICALP
- Infinity 1996, Pisa, Italy with CONCUR