Publications

 We present a methodology for modelling population dynamics with formal means of computer science. This allows unambiguous description of systems and application of analysis tools such as simulators and model checkers. In particular, the dynamics of a population of Aedes albopictus (a species of mosquito) and its modelling with the Stochastic Calculus of Looping Sequences (Stochastic CLS) are considered. The use of Stochastic CLS to model population dynamics requires an extension which allows environmental events (such as changes in the temperature and rainfalls) to be taken into account. A simulator for the constructed model is developed via translation into the specification language Maude, and used to compare the dynamics obtained from the model with real data.

Health information systems (HIS) are becoming increasingly integrated through network communication technologies. Integration aims at supporting collaborative healthcare workflows (CHWF) for improvement in sharing healthcare information and resources, efficiency of services and patients safety. CHWF are inherently complex, involving interactions among human actors, and (legacy) digital and physical systems. They are mission safety critical, privacy sensitive, and open to changes of requirements and environments. The complexity makes the definition, understanding, analysis, management, and monitoring of CHWF a software engineering challenge. We propose an approach to formal modelling and analysis of CHWF. The main problems that the approach addresses are abstraction and separation of concerns through algebraic manipulation. We use the CSP process algebra for modeling and verifying the dynamic interaction behavior of processes, and discuss the relation between the dynamic model and the static model of healthcare cases and resources. We also follow the idea of UML of some visualized models, but definitions of the syntax and semantics of these graphical models and their relation to the CSP models are left for future work.

Bayesian networks use the techniques of probability theory to reason under conditions of uncertainty. We investigated the use of Bayesian networks for radiological decision support. A Bayesian network for the interpretation of mammograms (MammoNet) was developed based on five patient­history features, two physical findings, and 15 mammographic features extracted by experienced radiologists. Conditional­probability data, such as sensitivity and specificity, were derived from peer­reviewed journal articles and from expert opinion. In testing with a set of 77 cases from a mammography atlas and a clinical teaching file, MammoNet performed well in distinguishing between benign and malignant lesions, and yielded a value of 0.881 (± 0.045) for the area under the receiver operating characteristic curve. We conclude that Bayesian networks provide a potentially useful tool for mammographic decision support.

Clinical decision analysis seeks to identify the optimal management strategy by modelling the un­ certainty and risks entailed in the diagnosis, natu­ ral history, and treatment of a particular problem or disorder. Decision trees are the most frequently used model in clinical decision analysis, but can be tedious to construct, cumbersome to use, and computationally prohibitive, especially with large, complex decision problems. We present a new method for clinical decision analysis that combines the techniques of decision theory and artificial in­ telligence. Our model uses a modular represen­ tation of knowledge that simplifies model building and enables more fully automated decision mak­ ing. Moreover, the model exploits problem struc­ tures to yield better computational efficiency. As an example we apply our techniques to the problem of management of acute deep venous thrombosis.

In order to precisely analyze healthcare workflows, we examine how healthcare workflows can be modeled and verified with an elementary and concise timed CSP extension. To avoid considering healthcare workflows in isolation, we investigate the usage of our CSP dialect for formally modeling workflows alongside the instruction model of the openEHR specification set, which is a general, maintainable, and interoperable approach to electronic health records. Hence, we present a CSP model for openEHR instructions, which allows timed reasoning, and also integrates a basic notion of data and undefinedness. We show that this CSP dialect is suited to verify important properties of healthcare workflows, like workflow consistency, checking against timed specifications, and resource scheduling.

This paper discusses the problem of abstract­ ing conditional probabilistic actions. We identify two distinct types of abstraction: intra­action abstraction and inter­action ab­ straction. We define what it means for the abstraction of an action to be correct and then derive two methods of intra­action ab­ straction and two methods of inter­action ab­ straction which are correct according to this criterion. We illustrate the developed tech­ niques by applying them to actions described with the temporal action representation used in the drips decision­theoretic planner and we describe how the planner uses abstraction to reduce the complexity of planning.

We present a first­order logic of time, chance, and probability that is capable of expressing the four types of higher­order probability sentences relating subjective probability and objective chance at different times. We define a causal notion of objective chance and show how it can be used in conjunction with subjective probability to distinguish between causal and evidential correlation by distinguishing between conditions, events, and actions that 1) influence the agent's belief in chance and 2) the agent believes to influence chance. Furthermore, the semantics of the logic captures some commonsense inferences concerning objective chance and causality. We show that an agent's subjective probability is the expected value of its beliefs concerning objective chance. We also prove that an agent using this representation believes with certainty that the past cannot be causally influenced. To appear in IEEE SMC special issue on Higher­Order Probability.

Any anytime algorithm used for decision­making should have the property that it considers the most important aspects of the decision problem first. In this way, the algorithm can first eliminate disas­ trous decisions and recognize particularly advan­ tageous decisions, considering finer details if time permits. We view planning as a decision­making process and discuss the design of anytime algo­ rithms for decision­theoretic planning. In particu­ lar, we present an anytime decision­theoretic plan­ ning algorithm that uses abstraction to focus atten­ tion first on those aspects of a planning problem that have the highest impact on expected utility. We discuss control schemes for refining this behav­ ior and methods for automatically creating good abstractions.

Any anytime algorithm used for decision­making should have the property that it considers the most important aspects of the decision problem first. In this way, the algorithm can first eliminate disastrous decisions and recognize particularly ad­ vantageous decisions, considering finer details if time permits. We view planning as a decision­making process and discuss the design of anytime algorithms for decision­ theoretic planning. In particular, we present an anytime decision­theoretic planning algorithm that uses abstraction to focus attention first on those aspects of a planning problem that have the highest impact on expected utility. We discuss control schemes for refining this behavior and methods for automatically creating good abstractions.

We present an educational tool for bringing the information contained in a Bayesian network to the end user in an easily intelligible form. The banter shell is designed to tutor users in evaluation of hypotheses and selection of optimal diagnostic procedures. banter can be used with any Bayesian network containing nodes that can be classified into hypotheses, observations, and diagnostic procedures. The system enables one to present various types of queries to the network, to test one's ablity to select optimal diagnostic procedures, and to request explanations. We describe the system's capabil­ ities by illustrating how it functions with two structurally different network models of real­world medical problems.

Decision­theoretic refinement planning is a new technique for finding optimal courses of ac­ tion. The authors sought to determine whether this technique could identify optimal strate­ gies for medical diagnosis and therapy. An existing model of acute deep venous thrombosis (DVT) of the lower extremities was encoded for analysis by the drips decision­theoretic refinement planning system. The encoding represented 6,206 possible plans. The drips planner used abstraction techniques to eliminate 5,551 plans (89%) from consideration with­ out examining them explicitly. It determined that, given the parameters specified, the most cost­effective management strategy was ``no tests, no treatment.'' This result differed from the published result of ``perform ultrasonography, treat if positive''; drips had revealed an error in the reference article's manually constructed decision trees. We conclude that decision­theoretic planning is useful for examining large medical decision problems, and that it can help reduce errors introduced by manual construction of decision trees.