The Participants-as-Interfaces (PaI) approach to system composition suggests that participants in a system can be considered interfaces to the outside world. Given a set of systems, one participant per system is chosen to play the role of an interface. When systems are composed, these interface participants are replaced by gateways that communicate with each other by forwarding messages. The PaI approach for systems of asynchronously communicating finite state machines (CFSMs) has been exploited in the literature for binary composition where the forwarding policy is necessarily unique. In this paper we consider the case of multiple system composition and extend preliminary work to the case where interactions among gateways can be mediated by additional orchestrating participants that comply with a given connection model. We represent the interactions among gateways as CFSM systems (called orchestrated connection policies) and prove that a number of relevant communication properties (e.g. deadlock-freedom, reception-error-freedom) are preserved by orchestrated PaI multicomposition, provided that the orchestrated connection policy used also satisfies the communication property in question.
As a basic quantum algorithm, the Bernstein-Vazirani algorithm is based on the principles of superposition in quantum mechanics, demonstrating superior efficiency over classical computation in finding hidden strings. Due to the high complexity of quantum mechanics, the correctness of quantum algorithms is difficult to guarantee through traditional simulation methods. By contrast, the Bernstein-Vazirani algorithm’s fundamental concepts and mathematical structures can be formalized into logical expressions and verified by higher-order logical reasoning. In this paper, we formally model and verify the Bernstein-Vazirani algorithm in the HOL Light theorem prover. Meanwhile, to indicate the practical significance of our work, we analyze two realistic scenarios, the error correction in quantum key distribution and image encryption and decryption.
We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patternsis combined with inductive theorem proving to discharge inductive verification conditions that ensure useful symbolic state space reductions. An obvious combination is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible combination. In this paper we focus instead on a new deductive model checking methodology to verify invariants —including inductive invariants— of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle. Inductive verification conditions not discharged automatically by the oracle are dealt with by commands that refine some constrained patterns by useful semantic equivalences, and by using an inductive theorem prover in interactive mode. This methodology is demonstrated by means of concurrent system examples using two Maude tools working in tandem: the DM-Check narrowing-based symbolic model checker, and the NuITP inductive theorem prover.
This paper investigates nominal anti-unification, i.e., the problem of computing least general generalizations of terms in the presence of binding structures and freshness constraints. We extend this problem to account for equational theories, specifically associativity (A), commutativity (C), and their combination (AC), yielding the notion of anti-unification modulo a theory E. Solutions in this setting, called E-generalizations, must consider both, the syntactic structure of nominal terms, and the algebraic properties imposed by E. In the general case, the problem has no solution due to the unbounded supply of atoms. To obtain a finitary setting, we fix a finite set of atoms A and introduce a rule-based algorithm for computing E-generalizations where only atoms from A are allowed to appear. The algorithm includes dedicated rules for reasoning modulo E and systematically explores permutations of subterms, which may lead to exponential blow-up in the number of generalizations. Although the computed set is not minimal, we describe heuristics that lead to computing promising E-generalizations in reasonable time. We also give an implementation of our algorithm which can be used to explore different optimization strategies that improve efficiency in practice, up to archiving tractability.
Processes of opinion formation rooted in social dynamics can significantly contribute to the polarization of social, political, and democratic interaction. Opinion dynamic models are essential for understanding the impact of specific social factors on the acceptance or rejection of opinions. This extended paper builds upon the conference presentation documented in [1], introducing improvements and new opinion models that explore biases and collective human behaviors. It presents a framework based on concurrent set relations that formalizes, simulates, and analyzes social interaction systems with dynamic opinion models. Within this framework, standard models for social learning are realized as specific instances. Implemented in the Maude system as a fully executable rewrite theory, the framework enables a detailed examination of how agents' opinions can be influenced within a system. The authors report on new formalization of several and existing social learning models, exploring their relationships with different concurrency models. New experimentation involving reachability analysis, probabilistic simulation, and statistical model checking has been conducted. These experiments are crucial for validating significant properties related to dynamic opinion models in Maude, offering new insights into the mechanisms of opinion shaping in social interaction.
The aim of this work is to present counterpart-based quantified temporal logics from several points of view. We start by introducing a set-based semantics for a (first-order) linear temporal logic based on the counterpart paradigm, along with results on its positive normal form both in the case of partial functions and of (possibly duplicating) relations. Then, a categorical semantics of the logic is introduced by means of relational presheaves. Both the presentations of the logic via the positive normal form and its categorical semantics are formalised using the proof assistant Agda, and we highlight the crucial aspects of our implementation and the practical use of (quantified) temporal logics in a constructive proof assistant.
When testing a state-based system one might use a set of (negative) test cases in which each test case is a sequence of events that should not occur. Testing then involves executing the system under test (SUT) in order to check whether any of these disallowed sequences can occur. While testing using such sequences can be effective, they introduce a source of inefficiency: if a test case expects the SUT to produce output a after observing a sequence sigma and the SUT instead produces a different output a ' after sigma then testing with that test case did not show an error, because the SUT can autonomously produce outputs, and terminates because the test case only makes sense if the exact sequence is observed. This is a source of inefficiency if there is another test case that starts with sigma followed by a ': we could have continued evaluating whether the application of this second test case leads to an error. This paper considers scenarios in which events represent inputs, outputs, or the passing of discrete time. We show how a set of sequential test cases can be converted into an equivalent set of adaptive test cases, with adaptivity addressing the above source of inefficiency. The proposed approach has the potential to improve efficiency when using any test generation technique that returns negative sequential test cases.
Designing distributed systems to have predictable performance under all loads is difficult because of resource exhaustion, nonlinearity, and stochastic behaviour. Timeliness, defined as delivering results (sufficiently often) within a specified delay distribution, is a central aspect of predictable performance. In this paper, we consider the Delta Q Systems Development paradigm (Delta QSD, developed by PNSol), which computes timeliness by modelling systems observationally using so-called outcome expressions. An outcome expression is a compositional definition of a system's observed behaviour that shows the causal connections between its basic operations. Given the Delta QSD operations, we use outcome expressions to compute the stochastic behaviour of the whole system including its timeliness. This paper defines and proves algebraic equivalences of outcome expressions with respect to timeliness. We prove the correctness of previously-known equivalences. We also introduce new equivalences and prove their correctness for outcome expressions containing probabilistic choice, failure, synchronisation (first-to-finish and last-to-finish), and sequential composition operators. We show how to incorporate failure as a first-class citizen in outcome expressions by developing the relevant mathematics based on the use of improper random variables. The paper shows the practical usefulness of algebraic equivalences by studying the design of a memory system containing a local cache, a networked read with timeout, and the ability to retry. We compute the delay and failure behaviour of several versions of this system, using the equivalences to simplify computations. This work is part of an ongoing project to disseminate and build tool support for Delta QSD, to make it available to the wider community of system designers.
We develop a generic computational model that can be used effectively for establishing the existence of winning strategies for concrete finite combinatorial games. Our modelling is (equational) logic-based involving advanced techniques from algebraic specification, and it can be executed by equational programming systems such as those from the OBJ-family. We show how this provides a form of experimental mathematics for strategy problems involving combinatorial games. We do this by defining general methods and by illustrating these with case studies.
Binary multirelations form a model of alternating nondeterminism useful for analysing games, interactions of computing systems with their environments or abstract interpretations of probabilistic programs. We investigate this alternating structure with inner or demonic and outer or angelic choices in a relation-algebraic language extended with specific operations on multirelations that relate to the inner layer of alternation.
We present a kind inference algorithm for the FREEST programming language. The input to the algorithmis FREEST source code with (possibly part of) kind annotations replaced by kind variables. The algorithm infers concrete kinds for all kind variables. We ran the algorithm on the FREEST test suite by first replacing kind annotation on all type variables by fresh kind variables, and concluded that the algorithm correctly infers all kinds. Non surprisingly, we found out that programmers do not choose the most general kind in 20% of the cases.
Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce the novel Hoare-style program logic ℒ_A , which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows one to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules of ℒ_A have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.
A wide range of real-time systems, formalisms, and modeling languages can be naturally represented in rewriting logic as real-time rewrite theories. In this paper we propose a language in which the user can conveniently define execution strategies-including state-and history-dependent ones-for real-time rewrite theories in a modular way, by specifying: (i) how to apply instantaneous transitions; (ii) how to advance time in the system; and (iii) the interplay between instantaneous transitions and advancing time. The user can easily specify more "time sampling strategies" than those supported by the Real-Time Maude tool, and we identify a new time sampling strategy that provides both efficient and exhaustive analysis for many distributed realtime systems. We provide unbounded and time-bounded simulation, reachability analysis, and LTL model checking commands for real-time rewrite theories whose executions are constrained by the user-defined discrete and timed strategies. These analysis methods are implemented by defining a strategy which extends the user's strategy, so that all analysis boils down to standard Maude rewriting with strategies. We exemplify the use of our strategy language and our analyses on a round trip time protocol and a train door controller. Our work also provides analysis with respect to user-defined strategies for formalisms that can be seen as real-time theories; we illustrate this for timed automata. Finally, we compare the performance of standard Maude search, where the desired time sampling strategy has been hardcoded into the model, with our strategy-implemented reachability analyses on the CASH scheduling algorithm benchmark.
Context: Probabilistic model checkers rely heavily on sparse matrix-vector multiplication (SpMV) to analyze a given probabilistic model. SpMV is a compute-and memory-intensive task. Therefore, it adversely affects the scalability of probabilistic model checkers. Graphical processing units (GPUs) have been utilized to improve the speed of SpMV. The GPU-based SpMV compute time consists of two independent factors: (Factor 1) host-to-GPU memory transfer and (Factor 2) the actual GPU-based SpMV multiplication. While many researchers have focused on the importance of Factor 1, none have explored ways to minimize its impact on overall SpMV computation time. Objective: This paper proposes an approach to reduce the memory transfer-related latency by hiding the data transfer from the host to the GPU in the state-space exploration step of probabilistic model checking. Methods: This is achieved in two steps: 1) reserve the complete coalesced memory in the GPU, and 2) move chunks of the sparse matrix from the host to the reserved memory during state-space exploration. Results: We report on an open source prototypical implementation of our approach on a CUDAbased cuSPARSE API in STORM, a prominent probabilistic model checker. Conclusion: We empirically demonstrate that our approach reduces memory transfer latency by at least one order of magnitude. Additionally, for most of the benchmarks, our approach achieves computation times comparable to GPU-PRISM, a prominent probabilistic model checker.
A process algebra is proposed, whose semantics maps a term to a nondeterministic finite automaton (NFA, for short). We prove a representability theorem: for each NFA N, there exists a process algebraic term p such that its semantics is an NFA isomorphic to N. Moreover, we provide a concise axiomatization of language equivalence: two NFAs N1 and N2 recognize the same language if and only if the associated terms p1 and p2, respectively, can be equated by means of a set of axioms, comprising 7 axioms plus 3 conditional axioms, only.
To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work transforms a list of statements into rewrite rules in a stepwise manner, and proves the correctness along the transformation and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language consists of inference rules that define single transitions of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for simpler definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work as an example, we show the existence of an injective function from configurations of a given program to terms, and reformulate the transformation by means of the injective function. The injective function enables us to make a one-to-one correspondence between single small-step transitions and reduction steps, and provides bisimilarity between the program and transformed LCTRS, resulting in a simpler correctness proof.
P is a domain-specific language designed for specifying asynchronous, event-driven systems. Its computational model is based on actors, i.e., on communicating state machines. This paper presents a formal semantics of P using rewriting logic, extending the language's verification capabilities. Implemented in Maude, a rewriting logic language, this semantics enables automated analysis of P programs, including reachability analysis, LTL model checking, and statistical model checking. Through illustrative examples, this paper demonstrates how this formalization significantly enhances P's verification capacities in practical scenarios.
