- TAVer - software.imdea.org

meeting: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap
by Kyveli Doveri 04 Dec '23

04 Dec '23

Hello, For the next meeting, we will discuss the attached paper and I'll host the discussion. The meeting will take place in Room 349 on Monday, December 11th at noon. Abstract: We consider the language inclusion problem for timed automata: given two timed automata A and B, are all the timed traces accepted by B also accepted by A? While this problem is known to be undecidable, we show here that it becomes decidable if A is restricted to having at most one clock. This is somewhat sur- prising, since it is well-known that there exist timed automata with a single clock that cannot be complemented. The crux of our proof consists in reducing the language inclusion problem to a reachability question on an infinite graph; we then construct a suitable well-quasi-order on the nodes of this graph, which ensures the termination of our search algorithm. We also show that the language inclusion problem is decidable if the only con- stant appearing among the clock constraints of A is zero. Moreover, these two cases are essentially the only decidable instances of language inclusion, in terms of restricting the various resources of timed automata. See you, Kyveli

1 0

3rd meeting: The Covering and Boundedness Problems for Vector Addition Systems
by Chana Weil-Kennedy 14 Nov '23

14 Nov '23

Hi all, For our third meeting, we will discuss the attached paper and I'll host the discussion. The meeting will take place in Room 349 on Monday, November 27th at noon. Mini-intro: This is a classic paper of Petri net theory. Petri nets — or the equivalent model of VASS — are a popular model of concurrency with a number of applications in database theory, business processes, and more (see e.g. surveys below). One of the central decision problems for Petri nets is the coverability problem, that asks whether there is a run from a given initial configuration to some configuration with at least the counter values of a given target configuration. Coverability is useful in the verification of safety conditions. The paper I will present is Rackoff’s 1978 result that coverability is in EXPSPACE, proved by showing that if coverability holds then there exists a run of double-exponential length. Petri net surveys: https://dl.acm.org/doi/10.1145/2893582.2893585 <https://dl.acm.org/doi/10.1145/2893582.2893585> https://link.springer.com/content/pdf/10.1007/3-540-65306-6_20.pdf <https://link.springer.com/content/pdf/10.1007/3-540-65306-6_20.pdf> See you, Chana

1 0

2nd meeting: Learning regular sets from queries and counterexamples
by Pierre Ganty 05 Nov '23

05 Nov '23

Hi all, For our second meeting, we will discuss the attached paper and I'll host the discussion. The meeting will take place in Room 349 on Monday, November 13th at noon. The problem of identifying an unknown regular set from examples of its members and nonmembers is addressed. It is assumed that the regular set is presented by a minimally adequate Teacher, which can answer membership queries about the set and can also test a conjecture and indicate whether it is equal to the unknown set and provide a counterexample if not. (A counterexample is a string in the symmetric difference of the correct set and the conjectured set.) A learning algorithm L^* is described that correctly learns any regular set from any minimally adequate Teacher in time polynomial in the number of states of the minimum DFA for the set and the maximum length of any counterexample provided by the Teacher. It is shown that in a stochastic setting the ability of the Teacher to test conjectures may be replaced by a random sampling oracle, EX( ). A polynomial-time learning algorithm is shown for a particular problem of context-free language identification. See you, Pierre.

1 0

1st TAVer meeting: A Survival Guide to Presburger Arithmetic
by Alessio Mansutti 23 Oct '23

23 Oct '23

Hello, In the first TAVer meeting we will discuss the attached paper. I'll host the discussion. The meeting will take place in Room 349 on October 30 at 12:00. Abstract of the paper: The first-order theory of the integers with addition and order, commonly known as Presburger arithmetic, has been a central topic in mathematical logic and computer science for almost 90 years. Presburger arithmetic has been the starting point for numerous lines of research in automata theory, model theory and discrete geometry. In formal verification, Presburger arithmetic is the first-choice logic to represent and reason about systems with infinitely many states. This article provides a broad yet concise overview over the history, decision procedures, extensions and geometric properties of Presburger arithmetic. Best, Alessio

1 0

TAVer first meeting!
by Alessio Mansutti 20 Oct '23

20 Oct '23

Hello, Pierre and I would like to start the TAVer reading group on October 30 (Monday), at 12:00. We could all have lunch together after the reading group. Please let us know if you are unavailable at that time or you strongly prefer another time slot. To start things smoothly, Pierre and I will present the first two papers, unless someone volunteers. Best, Alessio

1 0

2025

2024

2023

TAVer

2025

2024

2023

TAVer ----- 2025 ----- April 2025 March 2025 February 2025 January 2025 ----- 2024 ----- December 2024 November 2024 October 2024 September 2024 August 2024 July 2024 June 2024 May 2024 April 2024 March 2024 February 2024 January 2024 ----- 2023 ----- December 2023 November 2023 October 2023

TAVer