View: session overviewtalk overview

16:00 | Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols |

17:15 | PRESENTER: Christian Alrabbaa ABSTRACT. Logic-based approaches to AI have the advantage that their behaviour can in principle be explained by providing their users with proofs for the derived consequences. However, if such proofs get very large, then it may be hard to understand a consequence even if the individual derivation steps are easy to comprehend. This motivates our interest in finding small proofs for Description Logic (DL) entailments. Instead of concentrating on a specific DL and proof calculus for this DL, we introduce a general framework in which proofs are represented as labeled, directed hypergraphs whose hyperedges correspond to single sound derivation steps. On the theoretical side, we investigate the complexity of deciding whether a certain consequence has a proof of size at most n along the following orthogonal dimensions: (i) the underlying proof system is polynomial or exponential; (ii) proofs may or may not reuse already derived consequences; and (iii) the number $n$ is represented in unary or binary. We have determined the exact worst-case complexity of this decision problem for all but one of the possible combinations of these options. On the practical side, we have developed and implemented an approach for generating proofs for expressive DLs based on the non-standard inference forgetting. We have evaluated this approach on a set of realistic ontologies and compared the proofs with proofs generated by the DL reasoner ELK, finding that forgetting-based proofs are often better w.r.t. different measures of proof complexity. |

17:35 | PRESENTER: Oyendrila Dobe ABSTRACT. In this paper, we study the parameter synthesis problem for probabilistic hyperproperties. A probabilistic hyperproperty stipulates quantitative dependencies among a set of executions. We, in particular, solve the following problem: given a probabilistic hyperproperty and discrete-time Markov chain with parametric transition probabilities, compute regions of parameter configurations that instantiate the Markov chain to satisfy the hyperproperty, and regions that lead to violation. We solve this problem for a fragment of the temporal logic HyperPCTL that allows expressing quantitative reachability relation among a set of computation trees. We illustrate the application of our technique in the areas of differential privacy, probabilistic nonintereference, and probabilistic conformance. |

17:55 | PRESENTER: Tarek Khaled ABSTRACT. In biology, Boolean networks are conventionally used to represent and simulate gene regulatory networks. The attractors are the subject of special attention in analyzing the dynamics of a Boolean network. They correspond to stable states and stable cycles, which play a crucial role in biological systems. In this work, we study a new representation of the dynamics of Boolean networks that are based on a new semantics used in answer set programming (ASP). Our work is based on the enumeration of all the attractors of asynchronous Boolean networks having interaction graphs which are circuits. We show that the used semantics allows to design a new approach for computing exhaustively both the stable cycles and the stable states of such networks. The enumeration of all the attractors and the distinction between both types of attractors is a significant step to better understand some critical aspects of biology. We applied and evaluated the proposed approach on randomly generated Boolean networks and the obtained results highlight the benefits of this approach, and match with some conjectured results in biology. |

17:15 | PRESENTER: Marcel Hark ABSTRACT. In the last years, several works were concerned with identifying classes of programs where termination is decidable. We consider triangular weakly non-linear loops (twn-loops) over a ring Z ≤ S ≤ R_A , where R_A is the set of all real algebraic numbers. Essentially, the body of such a loop is a single assignment (x_1, ..., x_d) ← (c_1 · x_1 + pol_1, ..., c_d · x_d + pol_d) where each x_i is a variable, c_i ∈ S, and each pol_i is a (possibly non-linear) polynomial over S and the variables x_{i+1}, ..., x_d. Recently, we showed that termination of such loops is decidable for S = R_A and non-termination is semi-decidable for S = Z and S = Q. In this paper, we show that the halting problem is decidable for twn-loops over any ring Z ≤ S ≤ R_A. In contrast to the termination problem, where termination on all inputs is considered, the halting problem is concerned with termination on a given input. This allows us to compute witnesses for non-termination. Moreover, we present the first computability results on the runtime complexity of such loops. More precisely, we show that for twn-loops over Z one can always compute a polynomial f such that the length of all terminating runs is bounded by f( || (x_1, ..., x_d) || ), where || · || denotes the 1-norm. As a corollary, we obtain that the runtime of a terminating triangular linear loop over Z is at most linear. |

17:35 | PRESENTER: Radu Iosif ABSTRACT. The entailment between separation logic formulae with inductive predicates, also known as symbolic heaps, has been shown to be decidable for a large class of inductive definitions. Recently, a 2-EXPTIME algorithm was proposed and an EXPTIME-hard bound was established; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines. |

17:55 | PRESENTER: A Dileep ABSTRACT. We generalize the definition of an Induction Model given by L. Henkin (1960). The main goal of the paper is to study reduction and equivalence between these Induction Models. We give a formal definition for these concepts and then prove a criterion which can be used to check when one Induction Model can be reduced to or is equivalent to another Induction Model. We also look at the base cases and generating functions which can give us an Induction Model. There are three cases which we look at depending on the structure of the generating functions (arbitrary, additive, multiplicative). |