Zobrazeno 1 - 10
of 71
pro vyhledávání: '"Sangnier, Arnaud"'
We study networks of processes that all execute the same finite state protocol and that communicate through broadcasts. The processes are organized in a graph (a topology) and only the neighbors of a process in this graph can receive its broadcasts.
Externí odkaz:
http://arxiv.org/abs/2406.15202
We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways: a process can broadcast one message to all other processes or send it to at most one other process. In both cases, if no pro
Externí odkaz:
http://arxiv.org/abs/2403.18591
We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control states accordin
Externí odkaz:
http://arxiv.org/abs/2307.04546
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
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
Autor:
Horn, Florian, Sangnier, Arnaud
We study networks of processes which all execute the same finite-state protocol and communicate thanks to a rendez-vous mechanism. Given a protocol, we are interested in checking whether there exists a number, called a cut-off, such that in any netwo
Externí odkaz:
http://arxiv.org/abs/2007.05789
We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that deci
Externí odkaz:
http://arxiv.org/abs/1706.08608
We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in a d
Externí odkaz:
http://arxiv.org/abs/1706.05193
Publikováno v:
Logical Methods in Computer Science, Volume 15, Issue 3 (September 30, 2019) lmcs:4657
We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one ano
Externí odkaz:
http://arxiv.org/abs/1609.06124
Autor:
Iosif, Radu, Sangnier, Arnaud
We study several decision problems for counter systems with guards defined by convex polyhedra and updates defined by affine transformations. In general, the reachability problem is undecidable for such systems. Decidability can be achieved by imposi
Externí odkaz:
http://arxiv.org/abs/1605.05836