-
Causal knowledge engineering: A case study from COVID-19
Authors:
Steven Mascaro,
Yue Wu,
Ross Pearson,
Owen Woodberry,
Jessica Ramsay,
Tom Snelling,
Ann E. Nicholson
Abstract:
COVID-19 appeared abruptly in early 2020, requiring a rapid response amid a context of great uncertainty. Good quality data and knowledge was initially lacking, and many early models had to be developed with causal assumptions and estimations built in to supplement limited data, often with no reliable approach for identifying, validating and documenting these causal assumptions. Our team embarked…
▽ More
COVID-19 appeared abruptly in early 2020, requiring a rapid response amid a context of great uncertainty. Good quality data and knowledge was initially lacking, and many early models had to be developed with causal assumptions and estimations built in to supplement limited data, often with no reliable approach for identifying, validating and documenting these causal assumptions. Our team embarked on a knowledge engineering process to develop a causal knowledge base consisting of several causal BNs for diverse aspects of COVID-19. The unique challenges of the setting lead to experiments with the elicitation approach, and what emerged was a knowledge engineering method we call Causal Knowledge Engineering (CKE). The CKE provides a structured approach for building a causal knowledge base that can support the development of a variety of application-specific models. Here we describe the CKE method, and use our COVID-19 work as a case study to provide a detailed discussion and analysis of the method.
△ Less
Submitted 20 March, 2024;
originally announced March 2024.
-
Verifying Liveness Properties of ML Programs
Authors:
M. M. Lester,
R. P. Neatherway,
C. -H. L. Ong,
S. J. Ramsay
Abstract:
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi's intersection type-based model checking technique. We show that an implementation of this alg…
▽ More
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi's intersection type-based model checking technique. We show that an implementation of this algorithm, THORS, performs well on a number of small examples and we demonstrate how it can be used to verify liveness properties of OCaml programs. Example properties include statements such as "all opened sockets are eventually closed" and "the lock is held until the file is closed".
△ Less
Submitted 24 December, 2020;
originally announced December 2020.
-
Bisimilarity in fresh-register automata
Authors:
Andrzej S. Murawski,
Steven J. Ramsay,
Nikos Tzevelekos
Abstract:
Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have…
▽ More
Register automata are a basic model of computation over infinite alphabets. Fresh-register automata extend register automata with the capability to generate fresh symbols in order to model computational scenarios involving name creation. This paper investigates the complexity of the bisimilarity problem for classes of register and fresh-register automata. We examine all main disciplines that have appeared in the literature: general register assignments; assignments where duplicate register values are disallowed; and assignments without duplicates in which registers cannot be empty. In the general case, we show that the problem is EXPTIME-complete. However, the absence of duplicate values in registers enables us to identify inherent symmetries inside the associated bisimulation relations, which can be used to establish a polynomial bound on the depth of Attacker-winning strategies. Furthermore, they enable a highly succinct representation of the corresponding bisimulations. By exploiting results from group theory and computational group theory, we can then show solvability in PSPACE and NP respectively for the latter two register disciplines. In each case, we find that freshness does not affect the complexity class of the problem. The results allow us to close a complexity gap for language equivalence of deterministic register automata. We show that deterministic language inequivalence for the no-duplicates fragment is NP-complete, which disproves an old conjecture of Sakamoto. Finally, we discover that, unlike in the finite-alphabet case, the addition of pushdown store makes bisimilarity undecidable, even in the case of visibly pushdown storage.
△ Less
Submitted 5 February, 2025; v1 submitted 13 May, 2020;
originally announced May 2020.
-
Defunctionalization of Higher-Order Constrained Horn Clauses
Authors:
Long Pham,
Steven J. Ramsay,
C. -H. Luke Ong
Abstract:
Building on the successes of satisfiability modulo theories (SMT), Bjørner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained Horn clauses has recently been extended to higher-order logic by Cathcart Burn et al. To exploit the remarkable efficiency of SMT solving, a natural approach to solv…
▽ More
Building on the successes of satisfiability modulo theories (SMT), Bjørner et al. initiated a research programme advocating Horn constraints as a suitable basis for automatic program verification. The notion of first-order constrained Horn clauses has recently been extended to higher-order logic by Cathcart Burn et al. To exploit the remarkable efficiency of SMT solving, a natural approach to solve systems of higher-order Horn constraints is to reduce them to systems of first-order Horn constraints. This paper presents a defunctionalization algorithm to achieve the reduction.
Given a well-sorted higher-order constrained Horn clause (HoCHC) problem instance, the defunctionalization algorithm constructs a first-order well-sorted constrained Horn clause problem. In addition to well-sortedness of the algorithm's output, we prove that if an input HoCHC is solvable, then the result of its defunctionalization is solvable. The converse also holds, which we prove using a recent result on the continuous semantics of HoCHC. To our knowledge, this defunctionalization algorithm is the first sound and complete reduction from systems of higher-order Horn constraints to systems of first-order Horn constraints.
We have constructed DefMono, a prototype implementation of the defunctionalization algorithm. It first defunctionalizes an input HoCHC problem and then feeds the result into a backend SMT solver. We have evaluated the performance of DefMono empirically by comparison with two other higher-order verification tools.
△ Less
Submitted 22 February, 2019; v1 submitted 8 October, 2018;
originally announced October 2018.
-
Higher-Order Constrained Horn Clauses and Refinement Types
Authors:
Toby Cathcart Burn,
C. -H. Luke Ong,
Steven J. Ramsay
Abstract:
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem con…
▽ More
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. Finally, we show that an extension of the decision problem in which refinement types are used directly as guards on existential quantifiers can be reduced to the original problem. This result can be used to show that properties of higher-order functions that are definable using refinement types are also expressible using higher-order constrained Horn clauses.
△ Less
Submitted 1 August, 2017; v1 submitted 17 May, 2017;
originally announced May 2017.
-
How Helpful is Colour-Cueing of PIN Entry?
Authors:
Karen Renaud,
Judith Ramsay
Abstract:
21st Century citizens are faced with the need to remember numbers of PINs (Personal Identification Numbers) in order to do their daily business, and they often have difficulties due to human memory limitations. One way of helping them could be by providing cues during the PIN entry process. The provision of cues that would only be helpful to the PIN owner is challenging because the cue should only…
▽ More
21st Century citizens are faced with the need to remember numbers of PINs (Personal Identification Numbers) in order to do their daily business, and they often have difficulties due to human memory limitations. One way of helping them could be by providing cues during the PIN entry process. The provision of cues that would only be helpful to the PIN owner is challenging because the cue should only make sense to the legitimate user, and not to a random observer. In this paper we report on an empirical study where we added colour to the PINpad to provide an implicit memory cue to PINpad users. We compared the impact of colour PINpads as opposed to grey ones. As expected, the ability to recall a PIN deteriorated significantly over time irrespective of the type of PINpad used. However, there was ultimately no improvement in the ability to recall PINs when using colour PINpads.
△ Less
Submitted 30 July, 2014;
originally announced July 2014.
