This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing (...) translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that greatly complicate or even prevent their applicability in some important cases. For instance, most techniques assume that communication between honest principals is controlled by a Dolev-Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a protocol that relies on a less unsecure channel (...) (e.g. a confidential channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as of complex security properties that are normally not handled by state-of-the-art security protocol analysers. By using our approach we have been able to formalise all the assumptions required by the ASW protocol for optimistic fair exchange and some of its key security properties. Besides the previously reported attacks on the protocol, we report a new attack on a patched version of the protocol. (shrink)

We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and (...) a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms. (shrink)

Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.

Model checking, a prominent formal method used to predict and explain the behaviour of software and hardware systems, is examined on the basis of reflective work in the philosophy of science concerning the ontology of scientific theories and model-based reasoning. The empirical theories of computational systems that model checking techniques enable one to build are identified, in the light of the semantic conception of scientific theories, with families of models that are interconnected by simulation relations. (...) And the mappings between these scientific theories and computational systems in their scope are analyzed in terms of suitable specializations of the notions of model of experiment and model of data. Furthermore, the extensively mechanized character of model-based reasoning in model checking is highlighted by a comparison with proof procedures adopted by other formal methods in computer science. Finally, potential epistemic benefits flowing from the application of model checking in other areas of scientific inquiry are emphasized in the context of computer simulation studies of biological information processing. (shrink)

We consider Guttman scales both from an algebraic and a statistical point of view. We present a duality between a class of algebras and Guttman scalable response structures, and show that the index of reproducibility is not always a reliable indicator for the Guttman scalability of a data set. Furthermore, we present a model checking procedure, and close with an example.

We investigate a SAT-based bounded model checking method for EMTLK that is interpreted over timed models generated by timed interpreted systems. In particular, we translate the existential model checking problem for EMTLK to the existential model checking problem for a variant of linear temporal logic, and we provide a SAT-based BMC technique for HLTLK. We evaluated the performance of our BMC by means of a variant of a timed generic pipeline paradigm scenario and a (...) timed train controller system. (shrink)

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model (...) class='Hi'>checking framework. (shrink)

We present a variant of ATL with incomplete information which includes the distributed knowledge operators corresponding to synchronous action and perfect recall. The cooperation modalities assume the use the distributed knowledge of coalitions and accordingly refer to perfect recall incomplete information strategies. We propose a model-checking algorithm for the logic. It is based on techniques for games with imperfect information and partially observable objectives, and involves deciding emptiness for automata on infinite trees. We also propose an axiomatic system (...) and prove its completeness for a rather expressive subset. As for the constructs left outside this completely axiomatised subset, we present axioms by which they can be defined in the subset on the class of models in which every state has finitely many successors and give a complete axiomatisation for a “flat” subset of the logic with these constructs included. (shrink)

There is considerable confusion about the role of p-values in statistical model checking. To clarify that point, I introduce the distinction between measures of surprise and measures of evidence which come with different epistemological functions. I argue that p-values, often understood as measures of evidence against a null model, do not count as proper measures of evidence and are closer to measures of surprise. Finally, I sketch how the problem of old evidence may be tackled by acknowledging (...) the epistemic role of surprise indices. (shrink)

This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem (...) that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2EXPTIME. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines. (shrink)

It is known that the full computation-tree logic CTL∗is an important base logic for model checking. The bisimulation theorem for CTL∗is known to be useful for abstraction in model checking. In this paper, thebisimulation theorems for two paraconsistent four-valued extensions 4CTL∗and 4LCTL∗of CTL∗are shown, and a translation from 4CTL∗into CTL∗ispresented. By using 4CTL∗and 4LCTL∗, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

Software-controlled bots, also called social bots, are computer programs that act like human users on social media platforms. Recent work on detection of social bots is dominated by machine learning approaches. In this paper we explore bot detection as a model checking problem. We introduce Temporal Network Logic which we use to specify social networks where agents can post and follow each other. In this logic we formalize different types of social bot behavior. These are formulas that are (...) satisfied in a model of a network with bots. We provide a simple algorithm to extract a logical model from a real-life social network. We show that we can reduce TNL to a fragment of linear temporal logic with past and use this to establish the computational efficiency of model checking for social bot detection. (shrink)

Body checking, characterized by the repeated visual or physical inspection of particular parts of one’s own body (e.g. thighs, waist, or upper arms) is one of the most prominent behaviors associated with eating disorders, particularly Anorexia Nervosa (AN). In this paper, we explore the explanatory potential of the Recalcitrant Fear Model of AN (RFM) in relation to body checking. We argue that RFM, when combined with certain plausible auxiliary hypotheses about the cognitive and epistemic roles of emotions, (...) is able to explain key characteristics of body checking, including how body checking behavior becomes habitual and compulsive. (shrink)

Growing opioid misuse in the United States has resulted in more children living with an adult with an opioid use history. Although an abundance of research has demonstrated a link between opioid misuse and negative parenting behaviors, few intervention efforts have been made to target this underserved population. The Family Check-Up has been tested in more than 25 years of research, across multiple settings, and is an evidence-based program for reducing risk behavior, enhancing parenting skills, and preventing the onset of (...) substance use. It is designed to motivate parents to engage in positive parenting practices and to change problematic parenting and has been tested across a variety of ages including early childhood and adolescence. It is highlighted in NIDA’s Principles of Substance Use Prevention for Early Childhood: A research-based guide as one of only three effective selective prevention programs for substance abuse among families with young children. Recently, we developed an online version of the FCU that has now been adapted for early childhood and families with opioid use histories. The online platform and telehealth model allow for wide-scale dissemination, ease of training with community providers, and increased public health reach for families in remote, rural areas. This is particularly important when targeting families with opioid misuse and addiction because there are high rates of addiction in remote areas, yet few services available. In this article, we describe the FCU Online and review new content in the model that targets a population of young adult parents with substance abuse histories, including opioid use. New modules include content focused on harm reduction for this high-risk population of parents, such as safety in the home, substance use while parenting, and managing conflict with partners and friends. (shrink)

Automated Software Testing (AST) using Model Checking is in this article epistemologically analysed in order to argue in favour of a model-based reasoning paradigm in computer science. Preliminarily, it is shown how both deductive and inductive reasoning are insufficient to determine whether a given piece of software is correct with respect to specified behavioural properties. Models algorithmically checked in Model Checking to select executions to be observed in Software Testing are acknowledged as analogical models which (...) establish isomorphic relations with the target system’s data set. Analogical models developed in AST are presented as abductive models providing hypothetical explanations to observed executions. The model assumption—algorithmic check—software testing process is understood as the abduction—deduction—induction process defining the selective abduction and turned to isolate a set of model-based hypotheses concerning the target system behaviours. A manipulative abduction process is finally recognized in the practice of adapting, abstracting and refining models that do not provide successful predictions. (shrink)

Developmental psychologists have often portrayed young children as stubborn autodidacts who ignore the testimony of others. Yet the basic design of the human cognitive system indicates an early ability to co-ordinate information derived from first-hand observation with information derived from testimony. There is no obvious tendency to favour the former over the latter. Indeed, young children are relatively poor at monitoring whether they learned something from observation or from testimony. Moreover, the processes by which children and adults understand and remember (...) a sequence of events appear to be similar, whether they witness that sequence or are told about it. Children’s early receptivity to testimony raises the question of whether and how children discern what testimony is reliable. Arguably, before the emergence of reflective judgement, children are equipped with a tacit filtering device. To be understood, any new piece of testimony typically needs to be consistent with, and integrated into, what is already known about the topic in question. Children’s impoverished knowledge base will make that integrative process relatively slow. Thus, children’s early ignorance may often save them from misplaced credulity.Author Keywords: Trust; Testimony; Sources ; Cognitive development; Situation model. (shrink)

Modern medicine, based on enormous progress in science and its applications, has lost dimensions of individualized treatment and compassion which traditionally were an essential part of physician’s service over the millennia in Eastern and Western cultures. Today diseases and symptoms, rather than persons, are treated, based on objective quality norms and inflexible payment schemes rather than the rather than persons. We present a checklist model for personalized health care, which has been successful in teaching and practice to reclaim lost (...) territory in treating patients as persons. (shrink)

This chapter contains sections titled: Santa, Genealogy, and History Power/Knowledge: The Gift That Keeps on Giving “He sees you when you're sleeping”: Foucault's Theory of Panopticism “He's making a list, he's checking it twice” Naughty or Nice: The True Meaning of Discipline The Archeology of Christmas.

Political fact-checkers evaluate the truthfulness of politicians’ claims. This paper contributes to an emerging scholarly debate on whether fact-checkers treat political parties differently in a systematic manner depending on their ideology (bias). We first examine the available approaches to analyze bias and then present a new approach in two steps. First, we propose a logistic regression model to analyze the outcomes of fact-checks and calculate how likely each political party will obtain a truth score. We test our model (...) with a sample of fact-checks from Newtral, a major Spanish fact-checker. Our model would signal bias under two assumptions: a) all political parties are on average equally accurate in their statements; b) the verification method gives precise instructions and is implemented systematically. We investigate this second assumption with a series of interviews with Newtral fact-checkers. We show that standard verification protocols are so loosely implemented that fact-checks reflect a set of journalistic decisions, rather than a bias in the statistical sense. We call for a more rigorous definition of verification methods as a pre-requisite for an unbiased assessment of politician’s claims. (shrink)

In the paper, we study the dynamics of coalitional ability by proposing an extension of coalition logic (CL). CL allows one to reason about what a coalition of agents is able to achieve through a joint action, no matter what agents outside of the coalition do. The proposed dynamic extension is inspired by dynamic epistemic logic, and, in particular, by action models. We call the resulting logic coalition action model logic (CAML), which, compared to CL, includes additional modalities for (...) coalitional action models. We investigate the expressivity of CAML, and provide a complexity characterisation of its model checking problem. (shrink)

In this paper, we investigate the social herding phenomenon known as informational cascades, in which sequential inter-agent communication might lead to epistemic failures at group level, despite availability of information that should be sufficient to track the truth. We model an example of a cascade, and check the correctness of the individual reasoning of each agent involved, using two alternative logical settings: an existing probabilistic dynamic epistemic logic, and our own novel logic for counting evidence. Based on this analysis, (...) we conclude that cascades are not only likely to occur but are sometimes unavoidable by "rational" means: in some situations, the group’s inability to track the truth is the direct consequence of each agent’s rational attempt at individual truth-tracking. Moreover, our analysis shows that this is even so when rationality includes unbounded higher-order reasoning powers, as well as when it includes simpler, non-Bayesian forms of heuristic reasoning. (shrink)

Many problems in Multi-Agent Systems (MASs) research are formulated in terms of the abilities of a coalition of agents. Existing approaches to reasoning about coalitional ability are usually focused on games or transition systems, which are described in terms of states and actions. Such approaches however often neglect a key feature of multi-agent systems, namely that the actions of the agents require resources. In this paper, we describe a logic for reasoning about coalitional ability under resource constraints in the probabilistic (...) setting. We extend Resource-bounded Alternating-time Temporal Logic (RB-ATL) with probabilistic reasoning and provide a standard algorithm for the model-checking problem of the resulting logic Probabilistic resource-bounded ATL (pRB-ATL). We implement model-checking algorithms and present experimental results using simple multi-agent model-checking problems of increasing complexity. (shrink)

Current research in Explainable AI includes post-hoc explanation methods that focus on building transparent explaining agents able to emulate opaque ones. Such agents are naturally required to be accurate and trustworthy. However, what it means for an explaining agent to be accurate and trustworthy is far from being clear. We characterize accuracy and trustworthiness as measures of the distance between the formal properties of a given opaque system and those of its transparent explanantes. To this aim, we extend Probabilistic Computation (...) Tree Logic with operators to specify degrees of accuracy and trustworthiness of explaining agents. We also provide a semantics for this logic, based on a multi-agent structure and relative model-checking algorithms. The paper concludes with a simple example of a possible application. (shrink)

Lewis proposed to test the validity of a modal thesis by checking whether its possible-world translation is a theorem of counterpart theory. However, that criterion fails to validate many standard modal laws, thus raising doubts about the logical adequacy of the Lewisian framework. The present paper considers systems of counterpart theory of increasing strength and shows how each can be motivated by exhibiting a suitable intended model. In particular, perfect counterpart theory validates all the desired modal laws and (...) therefore provides a way out of the logical objection. Finally, a weakening of perfect counterpart theory is put forward as a response to some metaphysical objections. (shrink)

Scientific research is almost always conducted by communities of scientists of varying size and complexity. Such communities are effective, in part, because they divide their cognitive labor: not every scientist works on the same project. Philip Kitcher and Michael Strevens have pioneered efforts to understand this division of cognitive labor by proposing models of how scientists make decisions about which project to work on. For such models to be useful, they must be simple enough for us to understand their dynamics, (...) but faithful enough to reality that we can use them to analyze real scientific communities. To satisfy the first requirement, we must employ idealizations to simplify the model. The second requirement demands that these idealizations not be so extreme that we lose the ability to describe real-world phenomena. This paper investigates the status of the assumptions that Kitcher and Strevens make in their models, by first inquiring whether they are reasonable representations of reality, and then by checking the models' robustness against weakenings of these assumptions. To do this, we first argue against the reality of the assumptions, and then develop a series of agent-based simulations to systematically test their effects on model outcomes. We find that the models are not robust against weakenings of these idealizations. In fact we find that under certain conditions, this can lead to the model predicting outcomes that are qualitatively opposite of the original model outcomes. (shrink)

This paper argues for the importance of inner speech in a proper understanding of the structure of human conscious experience. It reviews one recent attempt to build a model of inner speech based on a grammaticization model (Steels, 2003) and compares it with a self-regulation model here proposed. This latter model is located within the broader literature on the role of language in cognition and the inner voice in consciousness. I argue that this role is not (...) limited to checking the grammatical correctness of prospective utterances before they are spoken. Rather, it is a more broadly activity-structuring role, regulating and shaping the ongoing shape of human activity in the world. Through linking inner speech to the control of attention, I argue that the study of the functional role of inner speech should be a central area of analysis in our attempt to understand the development and qualitative character of human consciousness and that modelling can play a central role in that understanding. (shrink)