1,721,038 research outputs found
Towards the specification and verification of modal properties for structured systems
No full textSystem specification formalisms should come with suitable property specification languages and effective verification tools. We sketch a framework for the verification of quantified temporal properties of systems with dynamically evolving structure. We consider visual specification formalisms like graph transformation systems (GTS) where program states are modelled as graphs, and the program
behavior is specified by graph transformation rules. The state space of a GTS can be represented as a graph transition system (GTrS), i.e. a transition system with states and transitions labelled, respectively, with a graph, and with a partial morphism representing the evolution of state components. Unfortunately, GTrSs are prohibitively large or infinite even for simple systems, making verification intractable and hence calling for appropriate abstraction techniques
Statistical Model Checking of Python Agent-Based Models: An Integration of MultiVeStA and Mesa
Full text linkAgent-based models (ABM) consist of several heterogeneous agents interacting in a complex way, possibly mediated by spatial constraints or other aspects, giving rise to emergent behavior not directly expressed in the model itself. These aspects made ABMs widespread in several areas, including the social sciences. These models are typically too complex to be solved analytically, requiring to use simulation-based analyses. Often, especially in the social sciences, these simulation-based analyses are not automatic, and the number of performed simulations or simulation steps might be arbitrary. This might lead to replicability issues, to low statistical accuracy of the results, or just to wrong results. In computer science, simulation-based analyses can be automated, e.g., using statistical model checking. We present an integration of the statistical model checker MultiVeStA with Mesa, a python-based framework for modeling and analysing ABMs. We validate the integration by using two seminal ABMs from the social sciences. We analyze the famous Boids flock model, able to generate flocking behaviors of birds, with the transient and counterfactual analysis capabilities of MultiVeStA. We analyze the well-known Schelling model, able to generate social segregation behaviors, with the steady-state and ergodicity diagnostics capabilities of MultiVeStA. The contribution of this paper is not methodological. Rather, this is on the one hand a case study paper presenting an application of MultiVeStA. On the other hand, it is a step towards automating and making more reliable the simulation-based analysis of models written in the popular Mesa framework
RCR report for analysis of spatiotemporal properties of stochastic systems using TSTL
No full text"Analysis of Spatiotemporal Properties of Stochastic Systems Using TSTL" [1] proposes a three-valued spatiotemporal logic to enrich the analysis framework for Signal Spatiotemporal Logic previously developed by the authors. This allows one to reason on the evolution of the satisfaction of properties expressed in a spatiotemporal logic, providing additional insight on the behavior of the studied system. The approach has been validated on two case studies: the fire spread and evacuation models originally presented in [2], and a novel case study on privacy in a communication network. This replicated computation result report focuses on the artifact accompanying the article, consisting in a prototypical tool implementation of the techniques presented in the article, together with all files necessary to replicate the analysis performed thereof. The artifact is available at https://ludovicalv.github.io/TOMACS/. After a few iterations with the authors, I found that the artifact agrees with the guidelines on availability (Artifact Avaliable) and replicability (Results Replicated) dictated in https://www.acm.org/publications/policies/artifact-review-badging. The software was made available in an accessible archival repository, and thanks to the instructions provided in the accompanying webapge, it has been straightforward to replicate the experimental results from the article.</p
Reproducibility Report for the Paper: Efficient Non-Blocking Event Management for Speculative Parallel Discrete Event Simulation
No full textThis is a report on the reproducibility of the experiments in the paper "Efficient Non-Blocking Event Management for Speculative Parallel Discrete Event Simulation"presented at the 38th ACM SIGSIM conference on Principles of Advanced Discrete Simulation (PADS'24). The artifact got badges Artifacts Evaluated - Functional v1.1, Artifacts Available v1.1, and Results Reproduced v1.1. The Artifacts Evaluated Functional badge has been assigned since the artifact associated with the research is documented, consistent, complete, exercisable, and includes evidence of verification and validation. The Artifacts Available badge has been given since the authors made the artifact permanently available. Finally, the Result Replicated badge has been assigned because the results shown in the paper have been reproduced by persons other than the authors, using artifacts provided by the authors
Exploiting over- and under-approximations for infinite-state counterpart models
Full text linkSoftware systems with dynamic topology are often infini-testate. Paradigmatic examples are those modeled as graph transformation systems (GTSs) with rewrite rules that allow an unbounded creation of items. For such systems, verification can become intractable, thus calling for the development of approximation techniques that may ease
the verification at the cost of losing in preciseness and completeness. Both over- and under-approximations have been considered in the literature, respectively offering more and less behaviors than the original system. At the same time, properties of the system may be either preserved or
reflected by a given approximation. In this paper we propose a general notion of approximation that captures some of the existing approaches for GTSs. Formulae are specified by a generic quantified modal logic, one that also generalizes many specification logics adopted in the literature for GTSs. We also propose a type system to denote part of the formulae as either reflected or preserved, together with a technique that exploits
under- and over-approximations to reason about typed as well as untyped formula
State space c-reductions for concurrent systems in rewriting logic
No full textWe present c-reductions, a state space reduction technique.
The rough idea is to exploit some equivalence relation on states (possibly capturing system regularities) that preserves behavioral properties, and explore the induced quotient system. This is done by means of a canonizer
function, which maps each state into a (non necessarily unique) canonical representative of its equivalence class. The approach exploits the expressiveness of rewriting logic and its realization in Maude to enjoy several advantages over similar approaches: exibility and simplicity in
the definition of the reductions (supporting not only traditional symmetry reductions, but also name reuse and name abstraction); reasoning support for checking and proving correctness of the reductions; and automatization
of the reduction infrastructure via Maude's meta-programming
features. The approach has been validated over a set of representative case studies, exhibiting comparable results with respect to other tools
Replicated Computations Results (RCR) report for “A holistic approach for collaborative workload execution in volunteer clouds”
No full text“A Holistic Approach for Collaborative Workload Execution in Volunteer Clouds” [3] proposes a novel approach to task scheduling in volunteer clouds. Volunteer clouds are decentralized cloud systems based on collaborative task execution, where clients voluntarily share their own unused computational resources. By using simulation-based statistical analysis techniques—in particular, statistical model checking—the authors show that their approach can outperform existing distributed task scheduling algorithms in the case of computation-intensive workloads. The analysis considered a realistic workload benchmark provided by Google. This replicated computations results report focuses on the prototypical tool implementation used in the article to perform such analysis. The software was straightforward to install and use, and a representative part of the experimental results from the article could be reproduced in reasonable time using a standard laptop
A conceptual framework for adaptation
No full textIn this position paper we present a conceptual vision of adap-
tation, a key feature of autonomic systems. We put some stress on the role of control data and argue how some of the programming paradigms and models used for adaptive systems match with our conceptual framework
Counterpart semantics for a second-order mu-calculus
No full textWe propose a novel approach to the semantics of quantified μ-calculi, considering models where states are algebras; the evolution relation is given by a counterpart relation (a family of partial homomorphisms), allowing for the creation, deletion, and merging of components; and formulas are interpreted over sets of state assignments (families of substitutions, associating formula variables to state components). Our proposal avoids the limitations of existing approaches, usually enforcing restrictions of the evolution relation: the resulting semantics is a streamlined and intuitively appealing one, yet it is general enough to cover most of the alternative proposals we are aware of
- …
