Abstrakt. Vi studerar verifieringen av en ändlig kontinuerlig tids Markovkedja (CTMC) C mot en linjär realtidsspecifikation som ges som en deterministisk tidsinställd automaton (DTA) A med finita eller Muller acceptvillkor. Den centrala frågan som vi tar upp är: vad är sannolikheten för den uppsättning C-vägar som accepteras av A, dvs. sannolikheten för att C uppfyller A? Det visas att detta under finita acceptanskriterier motsvarar möjligheten att nå målet i en finit bitvis deterministisk Markov-process (PDP), medan det för Muller-acceptanskriterier sammanfaller med möjligheten att nå målet för terminal starkt anslutna komponenter i en sådan PDP. Kvalitativ verifiering visas uppgå till en grafanalys av PDP. Sannolikheten för nåbarhet i våra PDP kännetecknas då som den minsta lösningen av ett system av Volterra integral ekvationer av den andra typen och visas vara ungefärliga av lösningen av ett system av partiella differentialekvationer. För enklockas DTA kan detta integrala ekvationssystem omvandlas till ett system med linjära ekvationer där koefficienterna är lösningar för vanliga differentialekvationer. Eftersom koefficienterna i själva verket är övergående sannolikheter i CTMC innebär detta resultat att standardalgoritmer för CTMC-analys räcker för att verifiera enklockas DTA-specifikationer. 1998 ACM Ämnesklassificering: D.2.4.
I REF, med tanke på en kontinuerlig tid Markov Chain och en linjär realtidsfastighet som tillhandahålls som en deterministisk tidsinställd automaton, målet är att utvärdera sannolikheten för uppsättningen accepterade vägar.
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
{'venue': 'LMCS 7 (1:12) 2011', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}