Showing 1–3 of 3 results for author: Simacek, J

Optimizing an LTS-Simulation Algorithm (Technical Report)

Authors: Lukáš Holík, Jiří Šimáček

Abstract: When comparing the fastest algorithm for computing the largest simulation preorder over Kripke structures with the one for labeled transition systems (LTS), there is a noticeable time and space complexity blow-up proportional to the size of the alphabet of an LTS. In this paper, we present optimizations that suppress this increase of complexity and may turn a large alphabet of an LTS to an advanta… ▽ More When comparing the fastest algorithm for computing the largest simulation preorder over Kripke structures with the one for labeled transition systems (LTS), there is a noticeable time and space complexity blow-up proportional to the size of the alphabet of an LTS. In this paper, we present optimizations that suppress this increase of complexity and may turn a large alphabet of an LTS to an advantage. Our experimental results show significant speed-ups and memory savings. Moreover, the optimized algorithm allows one to improve asymptotic complexity of procedures for computing simulations over tree automata using recently proposed algorithms based on computing simulation over certain special LTS derived from a tree automaton. △ Less

Submitted 9 July, 2023; originally announced July 2023.

Report number: FIT-TR-2009-03

Journal ref: Lukáš Holík and Jiří Šimáček, Optimizing an LTS-simulation algorithm. Computing and Informatics, 2010(7):1337-1348, 2010

Fully Automated Shape Analysis Based on Forest Automata

Authors: Lukas Holik, Ondrej Lengal, Adam Rogalewicz, Jiri Simacek, Tomas Vojnar

Abstract: Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples of tree automata. In order to allow for representing complex heap graphs, the notion of FA allowed one to provide user-defined FA (called boxes) that encode repetitive graph patterns of shape graphs to be used as alphab… ▽ More Forest automata (FA) have recently been proposed as a tool for shape analysis of complex heap structures. FA encode sets of tree decompositions of heap graphs in the form of tuples of tree automata. In order to allow for representing complex heap graphs, the notion of FA allowed one to provide user-defined FA (called boxes) that encode repetitive graph patterns of shape graphs to be used as alphabet symbols of other, higher-level FA. In this paper, we propose a novel technique of automatically learning the FA to be used as boxes that avoids the need of providing them manually. Further, we propose a significant improvement of the automata abstraction used in the analysis. The result is an efficient, fully-automated analysis that can handle even as complex data structures as skip lists, with the performance comparable to state-of-the-art fully-automated tools based on separation logic, which, however, specialise in dealing with linked lists only. △ Less

Submitted 21 April, 2013; originally announced April 2013.

Comments: Accepted to CAV'13

The Tree Width of Separation Logic with Recursive Definitions

Authors: Radu Iosif, Adam Rogalewicz, Jiri Simacek

Abstract: Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we esta… ▽ More Separation Logic is a widely used formalism for describing dynamically allocated linked data structures, such as lists, trees, etc. The decidability status of various fragments of the logic constitutes a long standing open problem. Current results report on techniques to decide satisfiability and validity of entailments for Separation Logic(s) over lists (possibly with data). In this paper we establish a more general decidability result. We prove that any Separation Logic formula using rather general recursively defined predicates is decidable for satisfiability, and moreover, entailments between such formulae are decidable for validity. These predicates are general enough to define (doubly-) linked lists, trees, and structures more general than trees, such as trees whose leaves are chained in a list. The decidability proofs are by reduction to decidability of Monadic Second Order Logic on graphs with bounded tree width. △ Less

Submitted 30 March, 2013; v1 submitted 22 January, 2013; originally announced January 2013.

Comments: 30 pages, 2 figures