Author name cluster

Roberto Segala

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

1 author row

I&C Journal 2024 Journal Article

A computable and compositional semantics for hybrid systems

Davide Bresolin
Pieter Collins
Luca Geretti
Roberto Segala
Tiziano Villa
Sanja Živanović Gonzalez

Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterised faithfully using either discrete or continuous models only. Due to the intrinsic complexity of hybrid systems, it is highly desirable to describe them compositionally, where large systems are seen as the composition of several simpler subparts that are studied independently. Furthermore, since several problems, including reachability, are undecidable for hybrid systems, the availability of approximate decision procedures is another important feature. In this paper, we propose a purely behavioural formalism for hybrid systems that is compositional and supports approximate decision procedures. The formalism is abstract and sufficiently general to subsume or be a semantic framework for most of the concrete formalisms or languages proposed in the literature.

Details DOI

GandALF Workshop 2012 Workshop Paper

Modelling Implicit Communication in Multi-Agent Systems with Hybrid Input/Output Automata

Marta Capiluppi
Roberto Segala

We propose an extension of Hybrid I/O Automata (HIOAs) to model agent systems and their implicit communication through perturbation of the environment, like localization of objects or radio signals diffusion and detection. To this end we decided to specialize some variables of the HIOAs whose values are functions both of time and space. We call them world variables. Basically they are treated similarly to the other variables of HIOAs, but they have the function of representing the interaction of each automaton with the surrounding environment, hence they can be output, input or internal variables. Since these special variables have the role of simulating implicit communication, their dynamics are specified both in time and space, because they model the perturbations induced by the agent to the environment, and the perturbations of the environment as perceived by the agent. Parallel composition of world variables is slightly different from parallel composition of the other variables, since their signals are summed. The theory is illustrated through a simple example of agents systems.

PDF Details DOI

I&C Journal 2011 Journal Article

Probabilistic Logical Characterization

Holger Hermanns
Augusto Parma
Roberto Segala
Björn Wachter
Lijun Zhang

Probabilistic automata exhibit both probabilistic and non-deterministic choice. They are therefore a powerful semantic foundation for modeling concurrent systems with random phenomena arising in many applications ranging from artificial intelligence, security, systems biology to performance modeling. Several variations of bisimulation and simulation relations have proved to be useful as means to abstract and compare different automata. This paper develops a taxonomy of logical characterizations of these relations on image-finite and image-infinite probabilistic automata.

Details DOI

TCS Journal 2006 Journal Article

Dynamic load balancing with group communication

Shlomi Dolev
Roberto Segala
Alexander Shvartsman

This work considers the problem of efficiently performing a set of tasks using a network of processors in the setting where the network is subject to dynamic reconfigurations, including partitions and merges. A key challenge for this setting is the implementation of dynamic load balancing that reduces the number of tasks that are performed redundantly because of the reconfigurations. We explore new approaches for load balancing in dynamic networks that can be employed by applications using a group communication service (GCS). The GCS that we consider include a membership service (establishing new groups to reflect dynamic changes) but does not include maintenance of a primary component. For the n-processor, n-task load balancing problem defined in this work, the following specific results are obtained. For the case of fully dynamic changes including fragmentation and merges we show that the termination time of any on-line task assignment algorithm is greater than the termination time of an off-line task assignment algorithm by a factor greater than n / 12. We present a load balancing algorithm that guarantees completion of all tasks in all fragments caused by partitions with work O ( n + f · n ) in the presence of f fragmentation failures. We develop an effective scheduling strategy for minimizing the task execution redundancy and we prove that our strategy provides each of the n processors with a schedule of Θ ( n 1 / 3 ) tasks such that at most one task is performed redundantly by any two processors.

Details DOI

TCS Journal 2006 Journal Article

Switched PIOA: Parallel composition via distributed scheduling

Ling Cheung
Nancy Lynch
Roberto Segala
Frits Vaandrager

This paper presents the framework of switched probabilistic input/output automata (or switched PIOA), augmenting the original PIOA framework with an explicit control exchange mechanism. Using this mechanism, we model a network of processes passing a single token among them, so that the location of this token determines which process is scheduled to make the next move. This token structure therefore implements a distributed scheduling scheme: scheduling decisions are always made by the (unique) active component. Distributed scheduling allows us to draw a clear line between local and global nondeterministic choices. We then require that local nondeterministic choices are resolved using strictly local information. This eliminates unrealistic schedules that arise under the more common centralized scheduling scheme. As a result, we are able to prove that our trace-style semantics is compositional.

Details DOI

I&C Journal 2003 Journal Article

Hybrid I/O automata

Nancy Lynch
Roberto Segala
Frits Vaandrager

Hybrid systems are systems that exhibit a combination of discrete and continuous behavior. Typical hybrid systems include computer components, which operate in discrete program steps, and real-world components, whose behavior over time intervals evolves according to physical constraints. Important examples of hybrid systems include automated transportation systems, robotics systems, process control systems, systems of embedded devices, and mobile computing systems. Such systems can be very complex, and very difficult to describe and analyze. This paper presents the Hybrid Input/Output Automaton (HIOA) modeling framework, a basic mathematical framework to support description and analysis of hybrid systems. An important feature of this model is its support for decomposing hybrid system descriptions. In particular, the framework includes a notion of external behavior for a hybrid I/O automaton, which captures its discrete and continuous interactions with its environment. The framework also defines what it means for one HIOA to implement another, based on an inclusion relationship between their external behavior sets, and defines a notion of simulation, which provides a sufficient condition for demonstrating implementation relationships. The framework also includes a composition operation for HIOAs, which respects the implementation relation and a notion of receptiveness, which implies that an HIOA does not block the passage of time. The framework is intended to support analysis methods from both computer science and control theory. This work is a simplification of our earlier HIOA model. The main simplification in the new model is a clearer separation between the mechanisms used to model discrete and continuous interaction between components. In particular, the new model removes the dual use of external variables for discrete and continuous interactions.

Details DOI

TCS Journal 2002 Journal Article

Automatic verification of real-time systems with discrete probability distributions

Marta Kwiatkowska
Gethin Norman
Roberto Segala
Jeremy Sproston

We consider the timed automata model of Alur and Dill (Theoret. Comput. Sci. 126 (1994) 183–235), which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, it is often desirable to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, two approaches to model checking are introduced for this model. The first uses the algorithm of Baier and Kwiatkowska (Distributed Comput. 11 (1998) 125–155) to provide a verification technique against temporal logic formulae which can refer both to timing properties and probabilities. The second, generally more efficient, technique concerns the verification of probabilistic, real-time reachability properties.

Details DOI

I&C Journal 1998 Journal Article

Liveness in Timed and Untimed Systems

Roberto Segala
Rainer Gawlick
Jørgen Søgaard-Andersen
Nancy Lynch

When proving the correctness of algorithms in distributed systems, one generally considerssafetyconditions andlivenessconditions. The Input/Output (I/O) automaton model and its timed version have been used successfully, but have focused on safety conditions and on a restricted form of liveness called fairness. In this paper we develop a new I/O automaton model, and a new timed I/O automaton model, that permit the verification of general liveness properties on the basis of existing verification techniques. Our models include a notion ofreceptivenesswhich extends the idea ofreceptivenessof other existing formalisms, and enables the use of compositional verification techniques. The presentation includes anembeddingof the untimed model into the timed model which preserves all the interesting attributes of the untimed model. Thus, our models constitute acoordinated frameworkfor the description of concurrent and distributed systems satisfying general liveness properties.

Details DOI

I&C Journal 1997 Journal Article

Quiescence, Fairness, Testing, and the Notion of Implementation

Roberto Segala

Two formalisms for concurrency, the Input/Output automaton model and the theory of testing, are compared and are shown to have common foundations. The relationship between the fair and quiescent preorders of I/O automata is investigated and the two preorders are shown to coincide subject to some restrictions. I/O automata are encoded into the theory of testing and the reversedmustpreorder is shown to be equivalent to the quiescent preorder for strongly convergent, finitely branching I/O automata up to encoding. Conversely, a theory of testing is defined directly on I/O automata, and the new reversedmustpreorder is shown to coincide with the quiescent preorder on strongly convergent, finitely branching I/O automata.

Details DOI

TCS Journal 1995 Journal Article

A process algebraic view of input/output automata

Rocco De Nicola
Roberto Segala

Input/output automata are a widely used formalism for the specification and verification of concurrent algorithms. Unfortunately, they lack an algebraic characterization, a formalization which has been fundamental for the success of theories like CSP, CCS and ACP. We present a many-sorted algebra for I/O automata that takes into account notions such as interface, input enabling, and local control. It is sufficiently expressive for representing all finitely branching transition systems; hence, all I/O automata with a finitely branching transition relation. Our presentation includes a complete axiomatization of the external trace preorder relation over recursion-free processes with input and output.

Details DOI