Abstract-This paper gäller beräkningsmetoder för att verifiera egenskaper hos polyhedral invariant hybrid automata (PIHA), som är hybrid automata med diskreta övergångar som styrs av polyhedral vakter. För att verifiera egenskaperna hos statsbanorna för PIHA delas planaromkopplingsytorna upp för att definiera en ändlig uppsättning diskreta tillstånd i ett ungefärligt kvotövergångssystem (AQTS). Tillståndsövergångar i AQTS bestäms av de nåbara tillstånden, eller flödesledningar, som avger från kopplingsytorna i enlighet med den kontinuerliga dynamiken. I detta dokument presenteras en metod för beräkning av polyhedral approximationer till flödesrör. Det visas att flödesrörets approximationsfel kan göras godtyckligt litet för den allmänna ickelinjära dynamiken och att beräkningarna kan göras effektivare för affina system. Papperet beskriver också CheckMate, ett MATLAB-baserat verktyg för modellering, simulering och verifiering av hybridsystems egenskaper baserat på de beräkningsmetoder som tidigare beskrivits.
CheckMate-verktyget REF analyserar egenskaper hos hybridsystem som representeras av Simulink/State-flow-modeller med hjälp av en ändlig stat abstraktion av dynamiken.
Computational techniques for hybrid system verification
{'venue': 'IEEE Trans. Automat. Contr.', 'journal': 'IEEE Trans. Automat. Contr.', 'mag_field_of_study': ['Computer Science']}