thesis
Faster algorithms for alternating refinement relations
IST Austria Technical Report
published
Krishnendu
Chatterjee
author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X
Siddhesh
Chaubal
author
Pritish
Kamath
author
KrCh
department
One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.
https://research-explorer.app.ist.ac.at/download/5378/5489/IST-2012-0001_IST-2012-0001.pdf
application/pdfno
IST Austria2012
eng
2664-169010.15479/AT:IST-2012-0001
21
https://research-explorer.app.ist.ac.at/record/497
Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating refinement relations, IST Austria, 21p.
K. Chatterjee, S. Chaubal, and P. Kamath, <i>Faster algorithms for alternating refinement relations</i>. IST Austria, 2012.
Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. <i>Faster Algorithms for Alternating Refinement Relations</i>. IST Austria, 2012. <a href="https://doi.org/10.15479/AT:IST-2012-0001">https://doi.org/10.15479/AT:IST-2012-0001</a>.
Chatterjee, K., Chaubal, S., & Kamath, P. (2012). <i>Faster algorithms for alternating refinement relations</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2012-0001">https://doi.org/10.15479/AT:IST-2012-0001</a>
Chatterjee K, Chaubal S, Kamath P. <i>Faster Algorithms for Alternating Refinement Relations</i>. IST Austria; 2012. doi:<a href="https://doi.org/10.15479/AT:IST-2012-0001">10.15479/AT:IST-2012-0001</a>
K. Chatterjee, S. Chaubal, P. Kamath, Faster Algorithms for Alternating Refinement Relations, IST Austria, 2012.
Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Alternating Refinement Relations</i>. IST Austria, 2012, doi:<a href="https://doi.org/10.15479/AT:IST-2012-0001">10.15479/AT:IST-2012-0001</a>.
53782018-12-12T11:38:59Z2019-08-02T12:38:41Z