Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either only discrete or only continuous models. A good framework for hybrid systems should support their compositional description and analysis, since commonly systems are specified by a composition of smaller subsystems, to cope with the complexity of their monolithic representation. Moreover, since the reachability problem for hybrid systems is undecidable, one should investigate the conditions that guarantee approximate computability of composition, when only approximations to the exact problem data are available.

We illustrate the role of simulation relations in the process of verification of large concurrent and distributed systems, showing in particular how simulation relations can be used successfully for the analysis of security protocols.

We study simulation relations for probabilistic automata that require transitions to be matched up to negligible sets provided that computation lengths are polynomially bounded. These relations are meant to provide rigorous grounds to parts of correctness proofs for cryptographic protocols that are usually carried out by semi-formal arguments. We illustrate our ideas by recasting a correctness proof of Bellare and Rogaway based on the notion of matching conversation.

We describe the timed input/output automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new hybrid I/O automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and to express the important ideas of previous timed automata frameworks.

Network applications and services need to be environment-aware in order to meet non-functional requirements in increasingly dynamic contexts. We consider partition awareness as an instance of environment awareness in network applications that need to be reliable and self-managing. Partition-aware applications dynamically reconfigure themselves and adjust the quality of their services in response to partitioning and merging of networks. As such, they can automatically adapt to changes in the environment so as to remain available in multiple partitions without blocking, albeit with reduced or degraded functionality. We propose a system layer consisting of group membership and reliable multicast services that provides systematic support for partition-aware application development. We illustrate the effectiveness of the proposed interface by solving several problems that represent different classes of realistic network applications.

In [11] a method for the analysis of the expected time complexity of a randomized distributed algorithm is presented.

Abstract Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output automata; both safety and liveness properties are considered. A small but typical circuit is verified in both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I/O automata. An extended evaluation and comparison of the two methods is given.

Article Free Access Share on Proving time bounds for randomized distributed algorithms Authors: Nancy Lynch Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile , Isaac Saias Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile , Roberto Segala Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MAView Profile Authors Info & Claims PODC '94: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computingAugust 1994 Pages 314–323https://doi.org/10.1145/197917.198117Published:14 August 1994Publication History 45citation508DownloadsMetricsTotal Citations45Total Downloads508Last 12 Months10Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF