Showing 1–2 of 2 results for author: Ajspur, M

Optimised determinisation and completion of finite tree automata

Authors: John P. Gallagher, Mai Ajspur, Bishoksan Kafle

Abstract: Determinisation and completion of finite tree automata are important operations with applications in program analysis and verification. However, the complexity of the classical procedures for determinisation and completion is high. They are not practical procedures for manipulating tree automata beyond very small ones. In this paper we develop an algorithm for determinisation and completion of fin… ▽ More Determinisation and completion of finite tree automata are important operations with applications in program analysis and verification. However, the complexity of the classical procedures for determinisation and completion is high. They are not practical procedures for manipulating tree automata beyond very small ones. In this paper we develop an algorithm for determinisation and completion of finite tree automata, whose worst-case complexity remains unchanged, but which performs far better than existing algorithms in practice. The critical aspect of the algorithm is that the transitions of the determinised (and possibly completed) automaton are generated in a potentially very compact form called product form, which can reduce the size of the representation dramatically. Furthermore, the representation can often be used directly when manipulating the determinised automaton. The paper contains an experimental evaluation of the algorithm on a large set of tree automata examples. △ Less

Submitted 1 November, 2017; v1 submitted 11 November, 2015; originally announced November 2015.

Tableau-based decision procedure for the multi-agent epistemic logic with all coalitional operators for common and distributed knowledge

Authors: Mai Ajspur, Valentin Goranko, Dmitry Shkatov

Abstract: We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiabilit… ▽ More We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi-agent epistemic logic CMAEL(CD) with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for CMAEL(CD) and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of formulae of CMAEL(CD) and closes for every unsatisfiable input set of formulae. △ Less

Submitted 25 January, 2012; originally announced January 2012.

Comments: Substantially extended and corrected version of arXiv:0902.2125. To appear in: Logic Journal of the IGPL, special issue on Formal Aspects of Multi-Agent Systems

MSC Class: 03B35; 03B42; 03B70; 68T27; 68T15 ACM Class: F.4.1; I.2.4