Health Technology Assessment (HTA) is the field that evaluates medical technologies such as new drugs with the perspective of enabling their use. This process is done by modeling the scenarios with and without the drug and computing the possible outcomes of the introduction of a health technology at a particular national health system. This is done by considering structures composed of "Health states" which represent the dynamic evolution of a patient. Probabilistic state-transition models are used to model and study the impact of the technology, taking into account not only the efficacy but also budget costs. In this work we make use of PRISM - a symbolic probabilistic model checker - to approach a problem in this field. Moreover, we compare it with the methods currently used in order to show how formal tools can be applied and useful for purposes of HTA evaluations.

In the formal development of systems, a modeling formalism must account for scenarios of inconsistency, where requirements may either reinforce or contradict one another. A key challenge arises when dealing with different sources of information, or sources affected by external factors, that may lead to contradictory or incomplete information. To model such situations, we propose Paraconsistent Systems, where states evolve through two accessibility relations that weigh the evidence of a transition occurring or not. These weights come, parametrically, from a residuated lattice and capture different scenarios: consistency, when their sum equals the unit; vagueness, when the sum is less than the unit; and inconsistency, when the sum exceeds the unit. This talk will explore the motivation and framework behind these systems, presenting a modal logic to reason about them. Additionally, we introduce two notions of simulation and bisimulation-crisp and graded-used to relate Paraconsistent systems. Finally, results of modal invariance for specific subsets of formulas are discussed.

Designing and analysing hybrid systems, i.e., systems that mix discrete processes - such as deterministic programs - with continuous (and physical) behaviour - such as movement, velocity, and voltage - is difficult. Our approach to design and analyse such systems is to animate a basic calculus, using a c-like syntax, which includes statements where variables evolve based on systems of ordinary differential equations (ODEs). Our proof-of-concept tool is called Lince, which does not need to be installed, requiring only a web-browser. Using Lince we can quickly and easily obtain insights on hybrid systems based on a precise and formal semantics. This talk describes recent improvements to Lince and directions of future work. These improvements were driven by attempts to model concrete scenarios, which will be described in the talk, and by difficulties encountered during both the specification and the interpretation phases. More specifically, we enriched Lince with more operations, relaxed some language restrictions, improved error detection and reporting, introduced new visualisations mechanisms, and introduced a new numerical engine to complement the existing symbolic engine.

(Joint work with Rolf Hennicker and Alexandre Madeira)

Event/data-based systems are controlled by events, their local data state may change in reaction to events. Numerous methods and notations for specifying such reactive systems have been designed, though with varying focus on the different development steps and their refinement relations. We first briefly review some of such methods, like temporal/modal logic, TLA, Alloy, UML state machines, symbolic transition systems, CSP, synchronous languages, and Event-B with their support for parallel composition and refinement. We then present E↓-logic for covering a broad range of abstraction levels of event/data-based systems from abstract requirements to constructive specifications in a uniform foundation. E↓-logic uses diamond and box modalities over structured events adopted from dynamic logic, for recursive process specifications it offers (control) state variables and binders from hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. Constructive operational specifications given by state transition graphs can be characterised by a single E↓-sentence. Also a variety of implementation constructors is available in E↓-logic to support, among others, event refinement and parallel composition. Thus the whole development process can rely on E↓-logic and its semantics as a common basis.

Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. This presentation introduces an extension of this framework called approximate GKAT (aGKAT), which equips GKAT over a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning `à la KAT' proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. Finally we then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.