Problemet med modellkontroll av hybridsystem är en välkänd utmaning i forskarsamhället. De flesta av de befintliga metoderna och verktygen är begränsade till säkerhetsegenskaper, eller fungerar genom att omvandla hybridsystemet för att verifieras till en diskret och därmed förlora information om systemets kontinuerliga dynamik. I detta dokument presenterar vi en logik för att specificera komplexa egenskaper hos hybridsystem som kallas HyLTL, och vi visar hur det är möjligt att lösa modellkontrollproblem genom att omvandla formeln till en likvärdig hybridautomat. På så sätt reduceras problemet till ett tillgänglighetsproblem på hybridautomata som kan lösas med hjälp av befintliga verktyg.
Mer nyligen utvecklar Bresolin REF HyLTL, en tidslogik för modellkontroll av hybridsystem, och visar hur man löser modellkontrollproblemet genom att översätta formler till motsvarande hybridautomata.
HyLTL: a temporal logic for model checking hybrid systems
{'venue': 'EPTCS 124, 2013, pp. 73-84', 'journal': None, 'mag_field_of_study': ['Computer Science']}