All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Relaxed Cycle Condition Improves Partial Order Reduction

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00019497" target="_blank" >RIV/00216224:14330/07:00019497 - isvavai.cz</a>

  • Result on the web

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    Relaxed Cycle Condition Improves Partial Order Reduction

  • Original language description

    Partial order reduction is a method widely used for tackling the state space explosion problem. In this paper we focus on a theoretical refinement of a particular instance of the partial order reduction which is nowadays an inherent part of most tools for explicit state model checking of Linear Temporal Logic. This particular instance is represented as a set of conditions C0 through C3 which describe valid reductions of a state space. We propose a hierarchy of alternatives to the cycle condition C3. Inthis hierarchy we point out which alternatives guarantee a valid reduction with respect to LTL_X properties.

  • Czech name

    Oslabení podmínky na cykly zlepšující redukci pomocí reprezentantů

  • Czech description

    Redukce pomocí reprezentantů je metoda široce používaná na boj se stavovou explozí. V článku se zaměřujeme na teoretické zjemnění konkrétní instance této redukce pro logiku LTL. Tato instance je representována množinou podmínek C0 až C3 které popisují platné redukce stavového prostoru. Navrhujeme hierarchii alternativ k podmínce C3. V této hierarchii ukážeme které alternativy k C3 garantují platnou redukci vzhledem k LTL vlastnostem.

Classification

  • Type

    D - Article in proceedings

  • CEP classification

    IN - Informatics

  • OECD FORD branch

Result continuities

  • Project

    Result was created during the realization of more than one project. More information in the Projects tab.

  • Continuities

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Others

  • Publication year

    2007

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Data specific for result type

  • Article name in the collection

    3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007)

  • ISBN

    978-80-7355-077-6

  • ISSN

  • e-ISSN

  • Number of pages

    8

  • Pages from-to

    140

  • Publisher name

    FI MU, FIT VUT

  • Place of publication

    Znojmo, Czech Republic

  • Event location

    Znojmo, Czech Republic

  • Event date

    Jan 1, 2007

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article