Abstrakt. Ökat intresse för fastighetsbaserad design kräver effektiva tillfredsställande förfaranden för expressiva temporallogik, t.ex. EEE-standarden Property Specification Language (PSL). I detta dokument föreslår vi en ny strategi för tillfredsställandet av PSL-formler; vi följer den senaste tidens metoder för beslutsförfaranden för tillfredsställande Modulo-teori, som vanligtvis tillämpas på fragment av First Order Logic. Den underliggande intuitionen är att kombinera två samverkande sökmekanismer: å ena sidan söker vi efter uppdrag som tillfredsställer den booleska abstraktionen av problemet; å andra sidan åberopar vi en lösare för tidsmässig tillfredsställelse i samband med timliga formler som motsvarar uppdraget. Inom denna ram utforskar vi två riktningar. För det första kan aggressiva förenklingar tillämpas med tanke på den fasta polariteten hos varje begränsning i teorins lösare. För det andra analyserar vi idén om konfliktåteruppbyggnad: närhelst ett tillfredsställande uppdrag på den booleska abstraktionens nivå resulterar i ett tidsmässigt otillfredsställande problem, identifierar vi inkonsekventa undergrupper som kan användas för att utesluta eventuellt många andra uppdrag. Vi föreslår två metoder för att extrahera konfliktuppsättningar på samband av tidsmässiga formler (en baserad på BDD-baserad modellkontroll, och en baserad på SAT-baserade Simple Bounded Model Checking). Vi analyserar gränserna och fördelarna med tillvägagångssättet med en grundlig experimentell utvärdering.
Författarna till REF försökte också generalisera idén om otillfredsställande kärnor till fallet med tidslogik med hjälp av SAT-baserade begränsade modellkontroller.
Boolean abstraction for temporal logic satisfiability
{'venue': 'IN DAMM AND HERMANNS [11', 'journal': None, 'mag_field_of_study': ['Computer Science']}