We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.

Coalgebras for analytic functors uniformly model graph-like systems where the successors of a state may admit certain symmetries. Examples of successor structure include ordered tuples, cyclic lists and multisets. Motivated by goals in automata-based verification and results on thin trees, we introduce thin coalgebras as those coalgebras with only countably many infinite paths from each state. Our main result is an inductive characterisation of thinness via an initial algebra. To this end, we develop a syntax for thin behaviours and capture with a single equation when two terms represent the same thin behaviour. Finally, for the special case of polynomial functors, we retrieve from our syntax the notion of Cantor-Bendixson rank of a thin tree.

We describe a general approach to deriving linear-time logics for a wide variety of state-based, quantitative systems, by modelling the latter as coalgebras whose type incorporates both branching and linear behaviour. Concretely, we define logics whose syntax is determined by the type of linear behaviour, and whose domain of truth values is determined by the type of branching behaviour, and we provide two semantics for them: a step-wise semantics akin to that of standard coalgebraic logics, and a path-based semantics akin to that of standard linear-time logics. The former semantics is useful for model checking, whereas the latter is the more natural semantics, as it measures the extent with which qualitative properties hold along computation paths from a given state. Our main result is the equivalence of the two semantics. We also provide a semantic characterisation of a notion of logical distance induced by these logics. Instances of our logics support reasoning about the possibility, likelihood or minimal cost of exhibiting a given linear-time property.

Stepwise development supported by the Event-B formalism has been used in the domain of system design and verification. This refinement approach guarantees that safety properties are preserved, while additional reasoning is required to prove the preservation of liveness properties. Our previous work proposes to use real-time trigger-response properties to reason about liveness properties and timed properties in real-time systems. Conditions such as weak fairness assumptions, relative deadlock freedom, and conditional convergence are explored to eliminate Zeno behavior when modeling real-time systems. In this reasoning framework, some strong constraints do not apply to real-world cases. This paper extends our previous results by using strong fairness assumptions to relax these constraints. We present the proof obligations together with temporal properties to construct the theorems and proofs. Fairness assumptions are used to enforce real-time properties in Event-B models. The carrier-sense multiple access with collision detection protocol is used as a case study to illustrate the approach.

As the physical world evolves with time, safety-critical systems are usually used with time-dependent functionality. The design and implementation of real-time systems are challenging due to the complicated functional and timing requirements. Event - B formalization offers a stepwise development approach for specifying and verifying systems with mathematical techniques and tools. In this paper, we propose four realtime specification patterns, namely time response pattern, abort pattern, intermediate pattern and periodic pattern, to facilitate the specification of real-time properties in Event-B models. The proposed patterns are used in a dual-chamber pacemaker case study to specify and verify the timing cycles based on the requirements. The model is proved using the Rodin tool.

Humans and agents often need to work together and agree on collective decisions. Ensuring that autonomous systems work responsibly is complex especially when encountering dilemmas. This paper proposes a novel, systematic model checking approach to responsible decision making by a human-agent collective to ensure it is safe, controllable and ethical. Our approach, which is based on the MCMAS model checker, verifies the permissibility of an agent's actions by checking the decision-making behaviour against the logical formulae specified for safety, controllability and ethical behaviour. The verification results through counterexamples and simulation results can provide a judgement, and an explanation to the AI engineer of the reasons actions are refused or allowed.

Abstraction and refinement offer a stepwise development approach to managing complexity in system design. Based on our previous work that extends Event-B models with high level real-time trigger-response properties, this paper presents refinement semantics of timed systems using behavioral traces. Forward simulation, which is a proof technique for refinement, is used to verify the consistency between different refinement levels. To prove refinement of trace semantics, we construct intermediate traces from concrete traces with a mapping function and prove the intermediate trace without stuttering events and states are abstract traces. Fairness assumptions, relative deadlock freedom, and conditional convergence are adopted in refinement steps to eliminate Zeno behavior in timed models. Based on the semantics, we develop refinement rules and strategies to perform refinement on timed models and refine real-time trigger-response properties into sequential or alternative sub-timing properties with proofs.

Event-B is a formal method for system-level modelling and analysis, which uses logic and set theory to describe discrete labelled transition systems. Timed transition systems have been introduced to incorporate timing constraints on transitions to describe real-time behaviours of the system. This paper proposes an approach to modelling high level timing constraints between different transitions with a timed trigger-response property. We present trace semantics for the trigger-response property and timed trigger-response property. This semantics provides a precise definition of valid trigger-response behaviours in Event-B machines. Based on the semantics, we develop proof obligations on Event-B machines under which all the traces of a machine satisfy the trigger-response property and the timed trigger-response property.

We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Buchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naive algorithm for computing extents, under additional assumptions on the domain of truth values.

We consider state-based systems modelled as coalgebras whose type incorporates branching, and show that suitably adapting the definition of coalgebraic bisimulation yields a general and uniform account of the linear-time behaviour of a state in such a coalgebra. By moving away from a boolean univer se of truth values, our approach can measure the extent to which a state in a system with branching is able to exhibit a particular linear-time behaviour. This instantiates to measuring the probability of a specific behaviour occurring in a probabilistic system, or measuring the minimal cost of exhibiting a given behaviour in the case of weighted computations.

In the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many problems are encoded as parity games, which are then solved by the seminal algorithm by Jurdzinski. In this paper we identify the essence of this workflow to be the notion of progress measure, and formalize it in general, possibly infinitary, lattice-theoretic terms. Our view on progress measures is that they are to nested/alternating fixed points what invariants are to safety/greatest fixed points, and what ranking functions are to liveness/least fixed points. That is, progress measures are combination of the latter two notions (invariant and ranking function) that have been extensively studied in the context of (program) verification. We then apply our theory of progress measures to a general model-checking framework, where systems are categorically presented as coalgebras. The framework's theoretical robustness is witnessed by a smooth transfer from the branching-time setting to the linear-time one. Although the framework can be used to derive some decision procedures for finite settings, we also expect the proposed framework to form a basis for sound proof methods for some undecidable/infinitary problems.

We extend earlier work on linear time fixpoint logics for coalgebras with branching, by showing how propositional operators arising from the choice of branching monad can be canonically added to these logics. We then consider two semantics for the uniform modal fragments of such logics: the previously-proposed, step-wise semantics and a new semantics akin to those of path-based logics. We prove that the two semantics are equivalent, and show that the canonical choice made for resolving branching in these logics is crucial for this property. We also state conditions under which similar, non-canonical logics enjoy the same property - this applies both to the choice of a branching modality and to the choice of linear time modalities. Our logics allow reasoning about linear time behaviour in systems with non-deterministic, probabilistic or weighted branching. In all these cases, the logics enhanced with propositional operators gain in expressiveness. Another contribution of our work is a reformulation of fixpoint semantics, which applies to any coalgebraic modal logic whose semantics arises from a one-step semantics.

Applications of modal logics are abundant in computer science, and a large number of structurally different modal logics have been successfully employed in a diverse spectrum of application contexts. Coalgebraic semantics, on the other hand, provides a uniform and encompassing view on the large variety of specific logics used in particular domains. The coalgebraic approach is generic and compositional: tools and techniques simultaneously apply to a large class of application areas and can, moreover, be combined in a modular way. In particular, this facilitates a pick-and-choose approach to domain-specific formalisms, applicable across the entire scope of application areas, leading to generic software tools that are easier to design, to implement and to maintain. This paper substantiates the authors’ firm belief that the systematic exploitation of the coalgebraic nature of modal logic will not only have impact on the field of modal logic itself but also lead to significant progress in a number of areas within computer science, such as knowledge representation and concurrency/mobility.