Modelirovanie i Analiz Informatsionnykh Sistem
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Modelirovanie i Analiz Informatsionnykh Sistem, 2010, Volume 17, Number 4, Pages 78–87 (Mi mais38)  

The application of adaptive symmetry reduction for LTL model checking

I. V. Konnov, V. A. Zakharov

M. V. Lomonosov Moscow State University
References:
Abstract: Adaptive symmetry reduction is a technique which exploits the similarity of components in systems of regular structure. It helps to reduce the effect of state explosion when exploring reachable states of a system. It assumes the perfect symmetry of states initially and tracks symmetry violations on-the-fly by exploring an extended state space. In this paper we show that the technique is applicable to LTL model checking as well. To succeed in this we incorporate the operations over the extended state space into the classic double depth-first search algorithm. The nested search is modified to detect a feasible pseudo-cycle via an accepting state of Buchi automaton instead of a cycle. We show that the existence of a pseudo-cycle results in satisfiability of an Indexed LTL formula on a model of the system and vice versa. This result opens the way for implementing adaptive symmetry reduction in a LTL model checker.
Keywords: model checking, LTL, symmetry.
Received: 06.09.2010
Document Type: Article
UDC: 519.7
Language: Russian
Citation: I. V. Konnov, V. A. Zakharov, “The application of adaptive symmetry reduction for LTL model checking”, Model. Anal. Inform. Sist., 17:4 (2010), 78–87
Citation in format AMSBIB
\Bibitem{KonZak10}
\by I.~V.~Konnov, V.~A.~Zakharov
\paper The application of adaptive symmetry reduction for LTL model checking
\jour Model. Anal. Inform. Sist.
\yr 2010
\vol 17
\issue 4
\pages 78--87
\mathnet{http://mi.mathnet.ru/mais38}
Linking options:
  • https://www.mathnet.ru/eng/mais38
  • https://www.mathnet.ru/eng/mais/v17/i4/p78
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Моделирование и анализ информационных систем
    Statistics & downloads:
    Abstract page:237
    Full-text PDF :80
    References:37
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024