
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 accordingly. We focus here on a specific semantics, called non-blocking, where the process requesting a rendez-vous can change its state even if no process can respond to it. In this context, we study the parameterised coverability problem of a configuration, which consists in determining whether there is an initialnumber of processes and an execution allowing to reach a configuration bigger than a given one. We show that this problem is EXPSPACE-complete and can be solved in polynomial time if the protocol is partitioned into two sets of states, the states from which a process can request a rendez-vous and the ones from which it can answer one. We also prove that the problem of the existence of an execution bringing all the processes in a final state is undecidable in our context. These two problems can be solved in polynomial time with the classical rendez-vous semantics.
Long version of of a paper accepted at CONCUR 2023
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Parameterised verification, Theory of computation → Formal languages and automata theory, [INFO] Computer Science [cs], C.2.4; F.4.3, 004, Logic in Computer Science (cs.LO), F.4.3, Counter machines; Coverability; Parameterised verification, Coverability, C.2.4, Computer Science - Multiagent Systems, Counter machines, Multiagent Systems (cs.MA), ddc: ddc:004
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Parameterised verification, Theory of computation → Formal languages and automata theory, [INFO] Computer Science [cs], C.2.4; F.4.3, 004, Logic in Computer Science (cs.LO), F.4.3, Counter machines; Coverability; Parameterised verification, Coverability, C.2.4, Computer Science - Multiagent Systems, Counter machines, Multiagent Systems (cs.MA), ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
