Abstrakt. Nåbarhetsproblemet för tidsinställd automata frågar om det finns en väg från ett initialtillstånd till ett måltillstånd. Standardlösningen på detta problem innebär att beräkna zondiagram över automaton, som i princip kan vara oändligt. För att göra grafen ändlig, är zoner ungefärliga med hjälp av en extrapolering operatör. Av effektivitetsskäl i nuvarande algoritmer är extrapolering av en zon alltid en zon, och i synnerhet är den konvex. I detta dokument föreslår vi att man ska lösa problemet med tillgänglighet utan sådana extrapoleringsföretag. För att säkerställa uppsägning, tillhandahåller vi en effektiv algoritm för att kontrollera om en zon ingår i den så kallade region stängning av en annan. Även om det teoretiskt sett är bättre, kan stängning inte användas i standardalgoritmen eftersom en stängning av en zon kanske inte är konvex. En ytterligare fördel med det föreslagna tillvägagångssättet är att det gör det möjligt att beräkna approximativa parametrar på flygbanan under utforskningen av zongrafen, i motsats till de nuvarande metoder som gör det genom en statisk analys av automaton före utforskningen. Detta möjliggör ytterligare förbättringar i algoritmen. Lovande experimentella resultat presenteras.
I REF har det visat sig att det är möjligt att effektivt använda regionen stängning av ÜØÖ · ÄÍ, betecknad —Ó× till Ö · ÄÍ.
Using non-convex approximations for efficient analysis of timed automata
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science', 'Mathematics']}