An epistemic approach to the formal specification of statistical machine learning

We propose an epistemic approach to formalizing statistical properties of machine learning. Specifically, we introduce a formal model for supervised learning based on a Kripke model where each possible world corresponds to a possible dataset and modal operators are interpreted as transformation and testing on datasets. Then, we formalize various notions of the classification performance, robustness, and fairness of statistical classifiers by using our extension of statistical epistemic logic. In this formalization, we show relationships among properties of classifiers, and relevance between classification performance and robustness. As far as we know, this is the first work that uses epistemic models and logical formulas to express statistical properties of machine learning, and would be a starting point to develop theories of formal specification of machine learning.

An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic

Intuitionistic Propositional Logic is complete w.r.t. Kripke semantics: if a formula is not intuitionistically valid, then there exists a finite Kripke model falsifying it. The problem of obtaining concise models has been scarcely investigated in the literature. We present a procedure to generate minimal models in the number of worlds relying on Answer Set Programming (ASP).

Bisimulation for Secure Information Flow Analysis of Multi-Threaded Programs

Preserving the confidentiality of information is a growing concern in software development. Secure information flow is intended to maintain the confidentiality of sensitive information by preventing them from flowing to attackers. This paper discusses how to ensure confidentiality for multi-threaded programs through a property called observational determinism. Operational semantics of multi-threaded programs are modeled using Kripke structures. Observational determinism is formalized in terms of divergence weak low-bisimulation. Bisimulation is an equivalence relation associating executions that simulate each other. The new property is called bisimulation-based observational determinism. Furthermore, a model checking method is proposed to verify the new property and ensure that secure information flow holds in a multi-threaded program. The model checking method successively refines the Kripke model of the program until the quotient of the model with respect to divergence weak low-bisimulation is reached. Then, bisimulation-based observational determinism is checked on the quotient, which is a minimized model of the concrete Kripke model. The time complexity of the proposed method is polynomial in the size of the Kripke model. The proposed approach has been implemented on top of PRISM, a probabilistic model checking tool. Finally, a case study is discussed to show the applicability of the proposed approach.

Forcing and satisfaction in Kripke models of intuitionistic arithmetic

We define a class of first-order formulas $\mathsf{P}^{\ast }$ which exactly contains formulas $\varphi$ such that satisfaction of $\varphi$ in any classical structure attached to a node of a Kripke model of intuitionistic predicate logic deciding atomic formulas implies its forcing in that node. We also define a class of $\mathsf{E}$-formulas with the property that their forcing coincides with their classical satisfiability in Kripke models which decide atomic formulas. We also prove that any formula with this property is an $\mathsf{E}$-formula. Kripke models of intuitionistic arithmetical theories usually have this property. As a consequence, we prove a new conservativity result for Peano arithmetic over Heyting arithmetic.

Bi-Modal Naive Set Theory

This paper describes a modal conception of sets, according to which sets are 'potential' with respect to their members. A modal theory is developed, which invokes a naive comprehension axiom schema, modified by adding `forward looking' and `backward looking' modal operators. We show that this `bi-modal' naive set theory can prove modalized interpretations of several ZFC axioms, including the axiom of infinity. We also show that the theory is consistent by providing an S5 Kripke model. The paper concludes with some discussion of the nature of the modalities involved, drawing comparisons with noneism, the view that there are some non-existent objects.

Hintikka's World: Agents with Higher-order Knowledge

In this demonstration paper, we present a pedagogical tool called Hintikka's world for showing how artificial agents can reason about higher-order knowledge (an agent knows that another agent knows that...). The system provides famous AI examples such as Muddy children and Russian cards. The system also allows to implement user's own examples via the description of a Kripke model or via its generation by the generic tableau method prover MetTeL2.

Constraint-Based Modeling in Systems Biology

The idea of constraint-based modeling in systems biology is to describe a biological system by a set of constraints, i.e., by pieces of partial information about its structure and dynamics. Using constraint-based reasoning one may then draw conclusions about the possible system behaviors.In this talk, we will focus on constraint-based modeling techniques for regulatory networks starting from the discrete logical formalism of René Thomas. In this framework, logic and constraints arise at two different levels. On the one hand, Boolean or multi-valued logic formulae provide a natural way to represent the structure of a regulatory network, which is given by positive and negative interactions (i.e., activation and inhibition) between the network components. On the other hand, temporal logic formulae (e.g. CTL) may be used to reason about the dynamics of the system, represented by a state transition graph or Kripke model.

Reasoning about knowledge and messages in asynchronous multi-agent systems

We propose a variant of public announcement logic for asynchronous systems. To capture asynchrony, we introduce two different modal operators for sending and receiving messages. The natural approach to defining the semantics leads to a circular definition, but we describe two restricted cases in which we solve this problem. The first case requires the Kripke model representing the initial epistemic situation to be a finite tree, and the second one only allows announcements from the existential fragment. After establishing some validities, we study the model checking problem and the satisfiability problem in cases where the semantics is well-defined, and we provide several complexity results.

Models and reality*

Kripke models, interpreted realistically, have difficulty making sense of the thesis that there might have existed things that do not in fact exist, since a Kripke model in which this thesis is true requires a model structure in which there are possible worlds with domains that contain things that do not exist. This paper argues that we can use Kripke models as representational devices that allow us to give a realistic interpretation of a modal language. The method of doing this is sketched, with the help of an analogy with a Galilean relativist theory of spatial properties and relations.