We build on abduction-based explanations for machine learning and develop a method for computing local explanations for neural network models in natural language processing (NLP). Our explanations comprise a subset of the words of the input text that satisfies two key features: optimality w.r.t. a user-defined cost function, such as the length of explanation, and robustness, in that they ensure prediction invariance for any bounded perturbation in the embedding space of the left-out words. We present two solution algorithms, respectively based on implicit hitting sets and maximum universal subsets, introducing a number of algorithmic improvements to speed up convergence of hard instances. We show how our method can be configured with different perturbation sets in the embedded space and used to detect bias in predictions by enforcing include/exclude constraints on biased terms, as well as to enhance existing heuristic-based NLP explanation frameworks such as Anchors. We evaluate our framework on three widely used sentiment analysis tasks and texts of up to 100 words from SST, Twitter and IMDB datasets, demonstrating the effectiveness of the derived explanations.

This paper presents our next research related to the use of SMT techniques for the analysis of security protocols. The behaviours of users and their changing knowledge during an investigated protocol executions are modelled as networks of communicating timed automata. The time properties are defined as the reachability properties of some, properly indicated states in the product automaton. We can do it using specially described time conditions, that can express dependencies between defined as a reachability property of some, chosen states in automata network, the possibility of performing some desired protocol steps and filling time constraints that use generation time of timestamps and lifetimes or/and networks delays. For our experiments we use boolean and SMT encodings that are the basis for respectively, SAT-and SMT-based bounded model checking. For SMT, the runs in product automaton are translated into the quantifier-free first-order formula. So far, we have implemented a well known bounded model checking algorithm and evaluated it for Needham-Schroeder Public Key, Needham Schroeder Symmetric Key, Woo Lam Pi and Wide Mouth Frog protocols. Now we show the tests carried out for the group of four known from the literature security protocols. We also compared our new SMT-based approach with a previous, only SAT-based, technique. For experiments, we used Minisat SAT solver, Z3, Yices2, CVC4 and MathSAT SMT solvers.

We present a SAT-based bounded model checking (BMC) method for timed interpreted systems (TIS) and for properties expressible in the existential fragment of a Real-Time Computation Tree Logic with epistemic components (RTECTLK). We implemented the standard BMC algorithm and evaluated it for two multi-agent systems: a timed train controller system and a timed generic pipeline paradigm. We also compared our new SAT-based technique with an SMT-based technique. For experiments we used the SAT solvers YicesSAT and Cryptominisat5, and the SMT solvers Z3 and YicesSMT.

We investigate a quasi-optimal cost reachability problem for weighted timed automata. We use a translation to the satisfiability modulo theories (SMT) problem to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing the target location, its total cost belongs to the interval [ c; c + 1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of run is called k- quasi- optimal. We exemplify the use of our solution to the investigated problem by means of the weighted timed generic pipeline protocol and the weighted job shop scheduling problem, and we provide some preliminary experimental results.