1,721,879 research outputs found
A Logical Framework for Reasoning About Local and Global Properties of Collective Systems
No full textCollective adaptive systems (CAS) are composed of a large number of entities that interact with each other to reach local or global goals. Entities operate without any centralized control and should adapt their behavior to the changes in the environment where they operate. Due to the intricacies of these interactions and adaptation, it is difficult to predict the behavior of CAS. For this reason, formal tools are needed to specify and verify this behavior to ensure consistency, reliability, correctness, and safety properties. In this paper, we present a novel logical framework that permits specifying properties of CAS at both local and global levels: local properties refer to the behavior of individuals, while global properties refer to the whole system. An exact model checking algorithm, whose complexity is linear with the size of the formula and with the size of the model is also presented together with another one based on statistical model checking that permits handling systems composed by a large number of agents. Finally, a simple scenario is used to evaluate the advantages of the proposed approach
A SPATIAL LOGIC FOR SIMPLICIAL MODELS
Full text linkCollective Adaptive Systems often consist of many heterogeneous components typically organised in groups. These entities interact with each other by adapting their behaviour to pursue individual or collective goals. In these systems, the distribution of these entities determines a space that can be either physical or logical. The former is defined in terms of a physical relation among components. The latter depends on logical relations, such as being part of the same group. In this context, specification and verification of spatial properties play a fundamental role in supporting the design of systems and predicting their behaviour. For this reason, different tools and techniques have been proposed to specify and verify the properties of space, mainly described as graphs. Therefore, the approaches generally use model spatial relations to describe a form of proximity among pairs of entities. Unfortunately, these graph-based models do not permit considering relations among more than two entities that may arise when one is interested in describing aspects of space by involving interactions among groups of entities. In this work, we propose a spatial logic interpreted on simplicial complexes. These are topological objects, able to represent surfaces and volumes efficiently that generalise graphs with higher-order edges. We discuss how the satisfaction of logical formulas can be verified by a correct and complete model checking algorithm, which is linear to the dimension of the simplicial complex and logical formula. The expressiveness of the proposed logic is studied in terms of the spatial variants of classical bisimulation and branching bisimulation relations defined over simplicial complexes
YODA: Yet anOther agent Description lAnguage
No full textMulti-Agent Systems (MASs) consist of a large number of entities, or agents, that cooperate and compete with each other to reach local and global goals. Agents operate immersed in an environment that can affect their behaviour. To design and predict the behaviour of MASs, it is crucial to use tools that allow not only to specify the behaviour of the single agent but allow to take into account the enclosing environment and its effect on the agents. In this paper, the framework YODA (Yet anOther agent Description lAnguage) is presented. The proposed specification language permits describing an agent in terms of the action it can perform and that are selected according to its state and a set of variables (sensors) that are observed from the environment. Action execution can change the agent state. The proposed language is also equipped with syntactic constructs that permits describing the enclosing environment and its evolution in time. At each step, the resulting model evolves as the consequence of the interaction among agents and the environment. In the paper, some case studies are used to show how our proposal works
The metric linear-time branching-time spectrum on nondeterministic probabilistic processes
No full textBehavioral equivalences were introduced as a simple and elegant proof methodology for establishing whether the behavior of two processes cannot be distinguished by an external observer. The knowledge of observers usually depends on the observations that they can make on process behavior. Furthermore, the combination of nondeterminism and probability in concurrent systems leads to several interpretations of process behavior. Clearly, different kinds of observations as well as different interpretations lead to different kinds of behavioral relations, such as (bi)simulations, traces and testing. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes with respect to trace and testing semantics. We study the properties of these metrics, like compositionality (expressed in terms of the non-expansiveness property), and we compare their expressive powers. More precisely, we compare them also to (bi)simulation metrics, thus obtaining the first metric linear time – branching time spectrum
DisTL: A Temporal Logic for the Analysis of the Expected Behaviour of Cyber-Physical Systems
No full textThe behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to uncertainties. We propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Distribution Temporal Logic (DisTL), a novel temporal logic allowing us to specify properties on the expected behaviour of systems, and to include the presence of uncertainties in the specification. We equip DisTL with a robustness semantics and we prove it sound and complete w.r.t. the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we give a statistical model checking algorithm for DisTL specifications, and we apply our framework to a simple unmanned ground vehicle scenario
RobTL: Robustness Temporal Logic for CPS
Full text linkWe propose Robustness Temporal Logic (RobTL), a novel temporal logic for the specification and analysis of distances between the behaviours of Cyber-Physical Systems (CPS) over a finite time horizon. RobTL specifications allow us to measure the differences in the behaviours of systems with respect to various objectives and temporal constraints, and to study how those differences evolve in time. Specifically, the unique features of RobTL allow us to specify robustness properties of CPS against uncertainty and perturbations. As an example, we use RobTL to analyse the robustness of an engine system that is subject to attacks aimed at inflicting overstress of equipment
Stark: A Software Tool for the Analysis of Robustness in the unKnown Environment
No full textCyber-Physical Systems (CPSs) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are robust against perturbations, i.e., whether systems are able to function correctly even in perturbed circumstances. In this paper we present the Software Tool for the Analysis of Robustness in the unKnown environment (Stark), our Java tool for the specification, analysis and testing of robustness properties of CPSs. Stark includes: (i) a specification language for systems behaviour, perturbations, distances on systems behaviours, and properties of those distances; (ii) a module for the simulation of system behaviours and their perturbed versions; (iii) a module for the evaluation of distances between behaviours; (iv) a statistical model checker for formulae in the Robustness Temporal Logic (RobTL), a temporal logic for the specification and verification of properties on the evolution of distances between the behaviours of CPSs, and thus also of robustness properties
Fluid approximation of broadcasting systems
Full text linkNature-inspired paradigms have been proposed to design and forecast behaviour of open distributed systems, such as sensor networks and the internet of things. In these paradigms system behaviour emerges from (complex) interactions among a large number of agents. Modelling these interactions in terms of classical point-to-point communication is often not practical. This is due to the large scale and the open nature of the systems, which means that partners for point-to-point communication may not be available at any given time. Nevertheless the need for efficient formal verification of qualitative and quantitative properties of these systems is of utmost importance, especially given their proposed pervasive and transparent nature. CARMA is a recently proposed formal modelling language for open distributed systems, which is equipped with a broadcast communication in order to meet the communication challenges of such systems. The inclusion of quantitative information about the timing and probability of actions gives rise to models suitable for analysing questions such as the probability that information will achieve total coverage within a system, or the expected market share that might be gained by competing service providers relying on viral advertising. The ability to express models is not the only challenge, because the scale of the systems we are interested in often defies discrete state-based analysis techniques such as stochastic simulation. This is the problem that we address in this paper as we consider how to provide an efficient fluid approximation, supporting efficient and accurate quantitative analysis of large scale systems, for a language that incorporates broadcast communication
Provably correct implementation of the AbC calculus
Full text linkBuilding open, distributed systems while guaranteeing a specific behaviour is difficult because of the dynamicity of the operating environments and the complexity of the interactions of their components. The AbC calculus provides a novel communication mechanism to select interacting partners based on their runtime capabilities, making it naturally to model complex interactions and adaptive behaviour in such systems. The formal account of this calculus has enabled constructing formally verifiable models and proving their properties. In this paper, we i) propose an implementation of AbC using the Erlang language ii) formalize the operational semantics of our implementation; iii) propose a set of rules that given an AbC specification, automatically generate Erlang executable code; and iv) prove that the proposed translation is correct by establishing a simulation relation between source and target specifications. This enables us to guarantee that any property proved for a given AbC specification is preserved by the corresponding implementation
- …
