Syntetiseringen av styrenheter för diskreta händelsesystem, som infördes av Ramadge och Wonham, uppgår till att beräkna vinnande strategier i paritetsspel. Vi visar att det inom denna ram är möjligt att utvidga specifikationerna för de övervakade systemen och begränsningarna för kontrollanterna genom att uttrycka dem i modal μ-kalculus. För att uttrycka oobserverbarhetsbegränsningar föreslår vi en utvidgning av modal μ-kalculus där man kan ange om en kant på en graf är en slinga. Denna förlängda μ-calculus har fortfarande de intressanta egenskaperna hos den klassiska. I synnerhet är det lika med automata med loop testning. Problemen såsom tomhetstestning och eliminering av alternering kan lösas för sådan automata. Den metod som föreslås i detta dokument för att lösa ett kontrollproblem består i att omvandla detta problem till ett problem med tillfredsställande av en μ-kalculus formel så att uppsättningen modeller av denna formel är exakt den uppsättning kontroller som löser problemet. Denna omvandling bygger på en enkel konstruktion av kvoten av automata med loop testning av ett deterministiskt övergångssystem. Detta är tillräckligt för att hantera centraliserade kontrollproblem. Lösningen av decentraliserade kontrollproblem använder en mer involverad konstruktion av kvoten av två automata. Detta arbete utvidgar ram ram Ramadge och Wonham i två riktningar. Vi betraktar oändligt beteende och godtyckliga regelbundna specifikationer, medan standardramen endast behandlar specifikationer på uppsättningen av finita vägar av processer. Vi tillåter också dynamiska förändringar av uppsättningen observerbara och kontrollerbara händelser.
Till exempel i REF, författarna behandlar syntesen av styrenheter för diskreta händelsesystem genom att hitta en vinnande strategier för paritetsspel.
Games for synthesis of controllers with partial observation
{'venue': 'Theor. Comput. Sci.', 'journal': 'Theor. Comput. Sci.', 'mag_field_of_study': ['Computer Science']}