Nasser Saheb

I&C Journal 2006 Journal Article

Broadcast in the rendezvous model

• Philippe Duchon
• Nicolas Hanusse
• Nasser Saheb
• Akka Zemmari

In many large, distributed or mobile networks, broadcast algorithms are used to update information stored at the nodes. In this paper, we propose a new model of communication based on rendezvous and analyze a multi-hop distributed algorithm to broadcast a message in a synchronous setting. In the rendezvous model, two neighbors u and v can communicate if and only if u calls v and v calls u simultaneously. Thus nodes u and v obtain a rendezvous at a meeting point. If m is the number of meeting points, the network can be modeled by a graph of n vertices and m edges. At each round, every vertex chooses a random neighbor and there is a rendezvous if an edge has been chosen by its two extremities. Rendezvous enable an exchange of information between the two entities. We get sharp lower and upper bounds on the time complexity in terms of number of rounds to broadcast: we show that, for any graph, the expected number of rounds is between ln n and O(n 2). For these two bounds, we prove that there exist some graphs for which the expected number of rounds is either O(ln(n)) or Ω(n 2). For specific topologies, additional bounds are given.

LPAR Conference 2003 Conference Paper

An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems

• Jean-Michel Couvreur
• Nasser Saheb
• Grégoire Sutre

Most verification problems on finite systems may be formulated and solved optimally using automata based techniques. Nonetheless LTL verification of (finite) probabilistic systems, i. e. deciding whether a probabilistic system almost surely satisfies an LTL formula, remains one of the few exceptions to this rule. As a matter of fact, existing automata-based solutions to this problem lead to double EXPTIME algorithms, while Courcoubetis and Yannakakis provide an optimal one in single EXPTIME. In this study, we remedy this exception. Our optimal automata based method proceeds in two steps: we present a minimal translation from LTL to ω -automata and point out appropriate properties on these automata; we then show that checking whether a probabilistic system satisfies an ω -automaton with positive probability can be solved in linear time for this kind of automata. Moreover we extend our study to the evaluation of this probability. Finally, we discuss some experimentations with our implementation of these techniques: the ProbaTaf tool.

I&C Journal 2003 Journal Article

Analysis of a randomized rendezvous algorithm

• Yves Métivier
• Nasser Saheb
• Akka Zemmari

In this paper we propose and analyze a randomized algorithm to get rendezvous between neighbours in an anonymous graph. We examine in particular the probability to obtain at least one rendezvous and the expected number of rendezvous. We study the rendezvous number distribution in the cases of chain graphs, rings, and complete graphs. The last part is devoted to the efficiency of the proposed algorithm.

MFCS Conference 1978 Conference Paper

Probabilistic LCF

• Nasser Saheb