1,721,111 research outputs found
Preface
No full textPreface of Proceedings of ICTCS 2015, the 16th Italian Conference on Theoretical Computer Science
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
Context Aware Specification and Verification of Distributed Systems
No full textDistributed and mobile systems are typically composed of heterogeneous computational units that interact with each other following a predefined protocol. Process algebras and modal logics have been largely used as tools for specifying and verifying such kind of systems. However, to use these tools a complete system description has to be provided. This is not always possible. Indeed, even if the protocol governing the interactions among the system components is completely specified, the precise implementation of each component, as well as the number of network elements, is generally unknown. In this paper we present a set of formal tools that permits specifying systems by means of mixed specifications: a system is not considered in isolation, but under the assumption that the enclosing environment satisfies a given set of properties. A model-checking algorithm is also defined to verify whether considered specifications satisfy or not the expected properties. In the former case, it is also guaranteed that whenever the context is instantiated with components satisfying the assumptions, property satisfaction is preserved
Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers.
No full textInternational Symposium on Trustworthy Global Computing
Trustworthy Global Computing
10th International Symposium, TGC 2015 Madrid, Spain, August 31 – September 1, 2015 Revised Selected Paper
Coordination Models and Languages - 20th IFIP WG 6.1 International Conference, COORDINATION 2018, Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018, Madrid, Spain, June 18-21, 2018. Proceedings.
No full textThis book constitutes the proceedings of the 20th International Conference on Coordination Models and Languages, COORDINATION 2018, held in Madrid, Spain, in June 2018, as part of the 13th International Federated Conference on Distributed Computing Techniques, DisCoTec 2018.
The 12 full papers included in this volume were carefully reviewed and selected from 26 submissions. The papers cover a wide range of topics and techniques related to system coordination, including: actor-based coordination, tuple- based coordination, agent-oriented techniques, constraints- based coordination, and finally coordination based on shared spaces
Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems, FORECAST@STAF 2016, Vienna, Austria, 8 July 2016.
No full textCollective Adaptive Systems (CAS) consist of a large number of spatially distributed heterogeneous entities with decentralised control and varying degrees of complex autonomous behaviour that may be competing for shared resources even when collaborating to reach common goals. It is important to carry out thorough quantitative modelling and analysis and verification of their design to investigate all aspects of their behaviour before they are put into operation. This requires combinations of formal methods and applied mathematics which moreover scale to large-scale CAS. The primary goal of FORECAST is to raise awareness in the software engineering and formal methods communities of the particularities of CAS and the design and control problems which they bring
FlyFast: A Scalable Approach to Probabilistic Model-Checking Based on Mean-Field Approximation
No full textModel-checking is an effective formal verification technique that has also been extended to quantitative logics and models such as PCTL and DTMCs as well as CSL and CTMCs/CTMDPs. Unfortunately, the state-space explosion problem of classical model-checking algorithms affects also quantitative extensions. Mean-field techniques provide approximations of the mean behaviour of large population models. These approximations are deterministic: a unique value of the fractions of agents in each state is computed for each time instant. A drastic reduction of the size of the model is obtained enabling the definition of an efficient model-checking algorithm. This paper is a survey of work we have done in the last few years in the area of mean-field approximated probabilistic model-checking. We start with a brief description of FlyFast, an on-the-fly model checker we have developed for approximated bounded PCTL model-checking, based on mean-field population DTMC approximation. Then we show an example of use of FlyFast in the context of Collective Adaptive Systems. We also discuss two additional interesting front-ends for FlyFast; the first one is a translation from CTMC-based population models and (a fragment of) CSL that allows for approximate probabilistic model-checking in the continuous stochastic time setting; the second one is a translation from a predicate-based process interaction language that allows for probabilistic model-checking of models based on components equipped both with behaviour and with attributes, on which predicates are defined that can be used in component interaction primitives
Assume-Guarantee Verification of Concurrent Systems
No full textProcess algebras are a set of mathematically rigourous languages with well defined semantics that permit modelling behaviour of concurrent and communicating systems. Verification of concurrent systems within the process algebraic approach can be performed by checking that processes enjoy properties described by some temporal logic’s formulae. In this paper we present a formal framework that permits verifying properties of concurrent and communicating systems by using an assumption-guarantee approach. Each system component is not considered in isolation, but in conjunction with assumptions about the context of the component. In the paper we introduce a sound and complete proof system that permits verifying whether a process, when it is executed in an environment for which we provide some assumptions, satisfies a given formula. It is also ensured that property satisfaction is preserved whenever the context is partially instantiated (implemented) as a concrete process that verifies the assumptions we have for the environment
A Modal Logic for KLAIM
Full text linkKlaim is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities, and on allocation environments that associate logical localities to physical sites. This paper presents a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic (HML) and the ν-calculus, but has novel features that permit dealing with state properties to describe the effect of actions over the different sites. The logic is equipped with a consistent and complete proof system that enables one to prove properties of mobile systems
Property-Preserving Refinement of Concurrent Systems
No full textVerification of concurrent systems within the process algebraic approach can be performed by checking that processes enjoy properties described by formulae of a temporal logic. However, to use these approach a complete description of the considered system has to be provided. In a previous work we propose a formal framework based on an assumption-guarantee approach where each system component is not considered in isolation, but in conjunction with assumptions about the context of the component. In the present paper we propose a procedure to refine the set of context assumptions. In each of the refinement steps the environment is partially instantiated with a process algebraic term while formulae satisfaction is preserved
- …
