Zobrazeno 1 - 10
of 155
pro vyhledávání: '"Bollig, Benedikt"'
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 3 (July 2, 2024) lmcs:11538
We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the satisfiability problem for this logic is undecidable in general, we i
Externí odkaz:
http://arxiv.org/abs/2307.00831
Autor:
Ye, Lina, Khmelnitsky, Igor, Haddad, Serge, Barbot, Benoît, Bollig, Benedikt, Leucker, Martin, Neider, Daniel, Roy, Rajarshi
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 1 (March 20, 2024) lmcs:11472
Angluin's L$^*$ algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by numerous ran
Externí odkaz:
http://arxiv.org/abs/2306.08266
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 2 (June 12, 2024) lmcs:10394
We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable o
Externí odkaz:
http://arxiv.org/abs/2211.15913
Autor:
Khmelnitsky, Igor, Haddad, Serge, Ye, Lina, Barbot, Benoît, Bollig, Benedikt, Leucker, Martin, Neider, Daniel, Roy, Rajarshi
Publikováno v:
EPTCS 370, 2022, pp. 81-96
Angluin's L* algorithm learns the minimal (complete) deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by a la
Externí odkaz:
http://arxiv.org/abs/2209.10315
Publikováno v:
EPTCS 370, 2022, pp. 1-16
We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain which can be compared wrt. equality. As the satisfiability problem for this logic is undecidable in general, in a previou
Externí odkaz:
http://arxiv.org/abs/2209.10309
Publikováno v:
Logical Methods in Computer Science, Volume 18, Issue 1 (January 20, 2022) lmcs:7485
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e.
Externí odkaz:
http://arxiv.org/abs/2105.06723
We correct our proof of a theorem stating that satisfiability of frequency linear-time temporal logic is undecidable [TASE 2012].
Externí odkaz:
http://arxiv.org/abs/2010.00296
Autor:
Khmelnitsky, Igor, Neider, Daniel, Roy, Rajarshi, Barbot, Benoît, Bollig, Benedikt, Finkel, Alain, Haddad, Serge, Leucker, Martin, Ye, Lina
This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyz
Externí odkaz:
http://arxiv.org/abs/2009.10610
Publikováno v:
EPTCS 326, 2020, pp. 33-49
The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm's correct behavior. Previous work has focused on static networks with an a priori fix
Externí odkaz:
http://arxiv.org/abs/2002.07545
We study the synthesis problem for systems with a parameterized number of processes. As in the classical case due to Church, the system selects actions depending on the program run so far, with the aim of fulfilling a given specification. The difficu
Externí odkaz:
http://arxiv.org/abs/1910.14294