Optimizing an LTS-Simulation Algorithm

Type

journal article

Language

English

Authors

Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Šimáček Jiří, Ing., Ph.D., DITS (FIT)

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 notable time and space complexity blow-up proportional to the size of the alphabet of an LTS. In this paper, we present optimizations that lower this blow-up 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.

Keywords

simulation, labeled transition system, finite automata, tree automata

URL

http://www.cai.sk/ojs/index.php/cai/article/view/147

Annotation

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 notable time and space complexity blow-up proportional to the size of the alphabet of an LTS. In this paper, we present optimizations that lower this blow-up 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.

Published

2010

Pages

1337–1348

Journal

COMPUTING AND INFORMATICS, vol. 2010, no. 7, ISSN 1335-9150

UT WoS

000287768300018

BibTeX

@article{BUT76431,
  author="Lukáš {Holík} and Jiří {Šimáček}",
  title="Optimizing an LTS-Simulation Algorithm",
  journal="COMPUTING AND INFORMATICS",
  year="2010",
  volume="2010",
  number="7",
  pages="1337--1348",
  issn="1335-9150",
  url="http://www.cai.sk/ojs/index.php/cai/article/view/147"
}

Projects

Developement of techniques for automatic verification of programs with dynamic data structures, GACR, Postdoktorandské granty, GP201/09/P531, start: 2009-01-01, end: 2011-12-31, completed
Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems, GACR, Doktorské granty, GD102/09/H042, start: 2009-01-30, end: 2012-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running

Research groups

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Departments

Department of Intelligent Systems (DITS)