Abstract Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present , a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the tool, and our own bespoke input. We present a mature version of with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that outperforms its only competitor in this domain.

Abstract Autonomous multi-agent systems use different modes of communication to support their autonomy and ease of interaction. In order to enable modelling and reasoning about such systems, we need frameworks that combine many forms of communication. R-CHECK is a modelling, simulation, and verification environment supporting the development of multi-agent systems, providing attributed channelled broadcast and multicast communication. Another common communication mode is point-to-point, wherein agents communicate with each other directly. Capturing point-to-point through R-CHECK ’s multicast and broadcast is possible, but cumbersome and prone to interference. Here, we extend R-CHECK (and its underlying formal calculus ReCiPe ) with bidirectional attributed point-to-point communication, which can be established based on identity or properties of participants. Moreover, we provide a compositional semantics that clearly describes how different modes of interaction co-exist without interference. We also support model-checking of point-to-point interactions by extending linear temporal logic with observation descriptors related to the participants in this communication mode. We argue that these extensions simplify the design, and demonstrate their benefits by means of an illustrative case study.

Abstract Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. Existing approaches struggle with this problem, or can handle at most deterministic games with Büchi goals. This work goes beyond by contributing the first effectual approach to synthesis with full LTL objectives, based on Boolean abstractions that encode both safety and liveness properties of the underlying infinite arena. We take a CEGAR approach: attempting synthesis on the Boolean abstraction, checking spuriousness of abstract counterstrategies through invariant checking, and refining the abstraction based on counterexamples. We reduce the complexity, when restricted to predicates, of abstracting and synthesising by an exponential through an efficient binary encoding. This also allows us to eagerly identify useful fairness properties. Our discrete synthesis tool outperforms the state-of-the-art on linear integer arithmetic (LIA) benchmarks from literature, solving almost double as many syntesis problems as the current state-of-the-art. It also solves slightly more problems than the second-best realisability checker, in one-third of the time. We also introduce benchmarks with richer objectives that other approaches cannot handle, and evaluate our tool on them.

One can find various temporal deontic logics in literature, most focusing on discrete time. The literature on real-time constraints and deontic norms is much sparser. Thus, many analysis techniques which have been developed for deontic logics have not been considered for continuous time. In this paper we focus on the notion of conflict analysis which has been extensively studied for discrete time deontic logics. We present a sound, but not complete algorithm for detecting conflicts in timed contract automata and prove the correctness of the algorithm, illustrating the analysis on a case study.

We present a translation from linear temporal logic with past to deterministic Rabin automata. The translation is direct in the sense that it does not rely on intermediate non-deterministic automata, and asymptotically optimal, resulting in Rabin automata of doubly exponential size. It is based on two main notions. One is that it is possible to encode the history contained in the prefix of a word, as relevant for the formula under consideration, by performing simple rewrites of the formula itself. As a consequence, a formula involving past operators can (through such rewrites, which involve alternating between weak and strong versions of past operators in the formula’s syntax tree) be correctly evaluated at an arbitrary point in the future without requiring backtracking through the word. The other is that this allows us to generalize to linear temporal logic with past the result that the language of a pure-future formula can be decomposed into a Boolean combination of simpler languages, for which deterministic automata with simple acceptance conditions are easily constructed.

Abstract Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interaction interfaces by forming collectives and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. In this article, we provide a modelling and analysis environment for the design of such system. Our tool offers simulation and verification to facilitate native reasoning about the domain concepts of such systems. We present our tool named R-CHECK (please find the associated toolkit repository here: https://github.com/dsynma/recipe ). R-CHECK supports a high-level input language with matching enumerative and symbolic semantics and provides modelling convenience for features such as reconfiguration, coalition formation, and self-organisation. For analysis, users can simulate the designed system and explore arising traces. Our included model checker permits reasoning about interaction protocols and joint missions.

Smart contracts have been proposed as executable implementations enforcing real-life contracts. Unfortunately, the semantic gap between these allows for the smart contract to diverge from its intended deontic behaviour. In this paper we show how a deontic contract can be used for real-time monitoring of smart contracts specifically and request-based interactive systems in general, allowing for the identification of any violations. The deontic logic of actions we present takes into account the possibility of action failure (which we can observe in smart contracts), allowing us to consider novel monitorable semantics for deontic norms. For example, taking a rights-based view of permissions allows us to detect the violation of a permission when a permitted action is not allowed to succeed. A case study is presented showing this approach in action for Ethereum smart contracts.

Natural language techniques have been employed in attempts to automatically translate legal texts, and specifically contracts, into formal models that allow automatic reasoning. However, such techniques suffer from incomplete coverage, typically resulting in parts of the text being left uninterpreted, and which, in turn, may result in the formal models failing to identify potential problems due to these unknown parts. In this paper we present a formal approach to deal with partiality, by syntactically and semantically permitting unknown subcontracts in an action-based deontic logic, with accompanying formal analysis techniques to enable reasoning under incomplete knowledge.

Although contract reparations have been extensively studied in the context of deontic logics, there is not much literature using reparations in automata-based deontic approaches. Contract automata is a recent approach to modelling the notion of contract-based interaction between different parties using synchronous composition. However, it lacks the notion of reparations for contract violations. In this article we look into, and contrast different ways reparation can be added to an automaton- and state-based contract approach, extending contract automata with two forms of such clauses: catch-all reparations for violation and reparations for specific violations.