Search

Your search keyword '"Lanotte, Ruggero"' showing total 115 results
Start Over Author "Lanotte, Ruggero"
115 results on '"Lanotte, Ruggero"'

104. Distributed Time-Asynchronous Automata.

Author

Hutchison, David, Kanade, Takeo, Kittler, Josef, Kleinberg, Jon M., Mattern, Friedemann, Mitchell, John C., Naor, Moni, Nierstrasz, Oscar, Pandu Rangan, C., Steffen, Bernhard, Sudan, Madhu, Terzopoulos, Demetri, Tygar, Doug, Vardi, Moshe Y., Weikum, Gerhard, Jones, Cliff B., Liu, Zhiming, Woodcock, Jim, Dima, Cătălin, and Lanotte, Ruggero

Abstract

We show that the class of distributed time-asynchronous automata is more expressive than timed automata, has a decidable emptiness problem, is closed under union, concatenation, star, shuffle and renaming, but not under intersection. The closure results are obtained by showing that distributed time-asynchronous automata are equivalent with a subclass of shuffle regular expressions and its related class of stopwatch automata. [ABSTRACT FROM AUTHOR]

Published
2007
Full Text
View/download PDF

105. Modeling Long-Running Transactions with Communicating Hierarchical Timed Automata.

Author

Gorrieri, Roberto, Wehrheim, Heike, Lanotte, Ruggero, Maggiolo-Schettini, Andrea, Milazzo, Paolo, and Troina, Angelo

Abstract

Long-running transactions consist of tasks which may be executed sequentially and in parallel, may contain sub-tasks, and may require to be completed before a deadline. These transactions are not atomic and, in case of executions which cannot be completed, a compensation mechanism must be provided. In this paper we develop a model of Hierarchical Timed Automata suitable to describe the aspects mentioned. The automaton-theoretic approach allows the verification of properties by model checking. As a case study, we model and analyze an example of long-running transaction. [ABSTRACT FROM AUTHOR]

Published
2006
Full Text
View/download PDF

106. Probabilistic Congruence for Semistochastic Generative Processes.

Author

Sassone, Vladimiro, Lanotte, Ruggero, and Tini, Simone

Abstract

We propose an SOS transition rule format for the generative model of probabilistic processes. Transition rules are partitioned in several strata, giving rise to an ordering relation analogous to those introduced by Ulidowski and Phillips for classic process algebras. Our rule format guarantees that probabilistic bisimulation is a congruence w.r.t. process algebra operations. Moreover, our rule format guarantees that process algebra operations preserve semistochasticity of processes, i.e. the property that the sum of the probability of the moves of any process is either 0 or 1. Finally, we show that most of operations of the probabilistic process algebras studied in the literature are captured by our format, which, therefore, has practical applications. [ABSTRACT FROM AUTHOR]

Published
2005

107. Taylor Approximation for Hybrid Systems.

Author

Morari, Manfred, Thiele, Lothar, Lanotte, Ruggero, and Tini, Simone

Abstract

We propose a new approximation technique for Hybrid Automata. Given any Hybrid Automaton H, we call Approx(H,k) the Polynomial Hybrid Automaton obtained by approximating each formula φ in H with the formulae φk obtained by replacing the functions in φ with their Taylor polynomial of degree k. We prove that Approx(H,k) is an over-approximation of H. We study the conditions ensuring that, given any ε > 0, some k0 exists such that, for all k>k0, the "distance" between any vector satisfying φk and at least one vector satisfying φ is less than ε. We study also conditions ensuring that, given any ε > 0, some k0 exists such that, for all k > k0, the "distance" between any configuration reached by Approx(H,k) in n steps and at least one configuration reached by H in n steps is less than ε. [ABSTRACT FROM AUTHOR]

Published
2005

109. Dynamic Hierarchical Machines.

Author

Burkhard, Hans-Dieter, Lindemann, Gabriela, Starke, Peter, Czaja, Ludwik, Lanotte, Ruggero, Maggiolo-Schettini, Andrea, Peron, Adriano, and Tini, Simone

Subjects
ROBOTICS, ROBOT programming, SEMANTICS, MACHINERY, OPERATIONS research
Abstract

We present Dynamic Hierarchical Machines (DHMs), an extension of Communicating Hierarchical Automata allowing dynamic activation of components. We give an operational semantics of DHMs and we provide examples of modeling in the context of security. We characterize a fragment of DHMs which are equivalent to Recursive Hierarchical Machines and therefore to Pushdown Machines. [ABSTRACT FROM AUTHOR]

Published
2003

110. Transformations of Timed Cooperating Automata.

Author

Lanotte, Ruggero, Maggiolo-Schettini, Andrea, Tini, Simone, and Peron, Adriano

Subjects
*MACHINE theory, *MATHEMATICAL models
Abstract

Investigates the transformation of timed cooperating automata (TCA). Variants of TCA and urgent TCA; Definition of transformation; Information on the three types of TCA transformations.

Published
2001

111. Automatic Analysis of a Non-Repudiation Protocol.

Author

Lanotte, Ruggero, Maggiolo-Schettini, Andrea, and Troina, Angelo

Subjects
COMPUTER network protocols, PROBABILITY theory, COMPUTER networks, COMPUTER science
Abstract

Abstract: We define a probabilistic model for the analysis of a Non-Repudiation protocol that guarantees fairness, without resorting to a trusted third party, by means of a probabilistic algorithm. By using the PRISM model checker, we estimate the probability for a malicious user to break the non-repudiation property, depending on various parameters of the protocol. [Copyright &y& Elsevier]

Published
2004
Full Text
View/download PDF

112. Internet of Things: A General Overview between Architectures, Protocols and Applications.

Author

Lombardi, Marco, Pascale, Francesco, Santaniello, Domenico, and Lanotte, Ruggero

Subjects
INTERNET of things, SMART cities, HUMAN ecology, INFORMATION sharing, HUMAN beings
Abstract

In recent years, the growing number of devices connected to the internet has increased significantly. These devices can interact with the external environment and with human beings through a wide range of sensors that, perceiving reality through the digitization of some parameters of interest, can provide an enormous amount of data. All this data is then shared on the network with other devices and with different applications and infrastructures. This dynamic and ever-changing world underlies the Internet of Things (IoT) paradigm. To date, countless applications based on IoT have been developed; think of Smart Cities, smart roads, and smart industries. This article analyzes the current architectures, technologies, protocols, and applications that characterize the paradigm. [ABSTRACT FROM AUTHOR]

Published
2021
Full Text
View/download PDF

113. Device Discovery and Context Registration in Static Context Header Compression Networks.

Author

Moons, Bart, De Poorter, Eli, Hoebeke, Jeroen, and Lanotte, Ruggero

Subjects
INTERNET protocol version 6, SENSOR networks, RECORDING & registration, ENERGY consumption, PAPER arts
Abstract

Due to the limited bandwidth of Low-Power Wide-Area Networks (LPWAN), the application layer is currently often tied straight above the link layer, limiting the evolution of sensor networks distributed over a large area. Consequently, the highly efficient Static Context Header Compression (SCHC) standard was introduced, where devices can compress the IPv6 and upper layer protocols down to a single byte. This approach, however, assumes that every compression context is distributed before deployment, again limiting the evolution of such networks. Therefore, this paper presents two context registration mechanisms leveraging on the SCHC adaptation layer. This is done by analyzing current registration solutions in order to find limitations and optimizations with regard to very constrained networks. Both solutions and the current State-of-The-Art (SoTA) are evaluated in a Lightweight Machine to Machine (LwM2M) environment. In such situation, both developed solutions decrease the energy consumption already after 25 transmissions, compared with the current SoTA. Furthermore, simulations show that Long Range (LoRa) devices still have a 80% chance to successfully complete the registration flow in a network with a 50% Packet Error Ratio. Briefly, the work presented in this paper delivers bootstrapping tools to constrained, SCHC-enabled networks while still being able to reduce energy consumption. [ABSTRACT FROM AUTHOR]

Published
2021
Full Text
View/download PDF

114. Equational Reasonings in Wireless Network Gossip Protocols

Author

Lanotte, Ruggero, Merro, Massimo, and Tini, Simone

Subjects
010201 computation theory & mathematics, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences
Abstract

Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout large-scale networks. In this paper, we propose a compositional analysis technique to study formal probabilistic models of gossip protocols expressed in a simple probabilistic timed process calculus for wireless sensor networks. We equip the calculus with a simulation theory to compare probabilistic protocols that have similar behaviour up to a certain tolerance. The theory is used to prove a number of algebraic laws which revealed to be very effective to estimate the performances of gossip networks, with and without communication collisions, and randomised gossip networks. Our simulation theory is an asymmetric variant of the weak bisimulation metric that maintains most of the properties of the original definition. However, our asymmetric version is particularly suitable to reason on protocols in which the systems under consideration are not approximately equivalent, as in the case of gossip protocols., Logical Methods in Computer Science ; Volume 14, Issue 3 ; 186-05974

115. On the Decidability of Linear Bounded Periodic Cyber-Physical Systems

Author

Ruggero Lanotte, Massimo Merro, Fabio Mogavero, Lanotte, Ruggero, Merro, Massimo, and Mogavero, Fabio

Subjects
Reachability problem, Model checking, Theoretical computer science, Computer Networks and Communications, Computer science, Process (engineering), Computation, 0211 other engineering and technologies, 02 engineering and technology, Cyber-physical system, 0202 electrical engineering, electronic engineering, information engineering, Isolation (database systems), Electrical and Electronic Engineering, Formal safety verification, Linear cyber-physical systems, Computer Science Applications1707 Computer Vision and Pattern Recognition, Control and Systems Engineering, 021103 operations research, Safety verification, Decidability, Bounded function, 020201 artificial intelligence & image processing, Verification and validation
Abstract

Cyber-Physical Systems (CPSs) are integrations of distributed computing systems with physical processes via a networking with actuators and sensors, where feedback loops among the components allow the physical processes to affect the computations and vice versa. Although CPSs can be found in several complex and sometimes critical real-world domains, their verification and validation often relies on simulation-test systems rather then automatic methodologies to formally verify safety requirements. In this work, we prove the decidability of the reachability problem for discrete-time linear CPSs whose physical process in isolation has a periodic behavior, up to an initial transitory phase.

Published
2019

Catalog

Books, media, physical & digital resources
See catalog results