Which of My Assumptions are Unnecessary for Realizability and Why Should I Care?

Specifications for reactive systems synthesis consist of assumptions and guarantees. However, some specifications may include unnecessary assumptions, i.e., assumptions that are not necessary for realizability. While the controllers that are synthesized from such specifications are correct, they are also inflexible and fragile; their executions will satisfy the specification's guarantees in only very specific environments.

In this work we show how to detect unnecessary assumptions, and to transform any realizable specification into a corresponding realizable core specification, one that includes the same guarantees but no unnecessary assumptions. We do this by computing an assumptions core, a locally minimal subset of assumptions that suffices for realizability. Controllers that are synthesized from a core specification are not only correct but, importantly, more general; their executions will satisfy the specification's guarantees in more environments.

We implemented our ideas in the Spectra synthesis environment, and evaluated their impact over different benchmarks from the literature. The evaluation provides evidence for the motivation and significance of our work, by showing (1) that unnecessary assumptions are highly prevalent, (2) that in almost all cases the fully-automated removal of unnecessary assumptions pays off in total synthesis time, and (3) that core specifications induce more general controllers whose reachable state space is larger but whose representation more memory efficient. Listing 2 SPECIFICATION: ROBOT EVADING MOVING OBSTACLE (CONT., ASSUMPTIONS AND GUARANTEES) 34 // The obstacle is initially docking 35 asm initiallyObstacleAtLowerRightCorner: 36 ini obsDock; 37 38 // The obstacle must not go forever without maintenance 39 asm obstacleMustDockInfinitelyOften: 40 alwEv obsDock; 41 42 // The obstacle is initially not waiting 43 asm initiallyObsWaitFalse: 44 ini !obsWait; 45 46 // The obstacle waits every other turn 47 asm obstacleWaitSwitches: 48 alw (obsWait->next(!obsWait))&(!obsWait->next(obsWait)); 49 50 // A waiting obstacle does not move 51 asm obstacleDoesNotMoveWhenObsWait: 52 alw obsWait->(next(obsX)=obsX & next(obsY)=obsY); 53 54 // The obstacle can move only one step in each direction 55 asm obstacleMovesAtMostOne: 56 alw moveObs(obsX) & moveObs(obsY); 57 58 // The robot is initially at top left corner 59 gar initiallyRobotAtTopLeftCorner: 60 ini robAt(1,1); 61 62 // The robot can move only one step in each direction 63 gar robotMovesAtMostOne: 64 alw moveRob(robX) & moveRob(robY); 65 66 // Robot never occupies obstacles's next position 67 gar robotAvoidsObstacle: 68 alw obsNotAt(robX,robY, next(obsX),next(obsY)); 69 70 // Robot never occupies obstacle cells 71 gar robotNotOnObstacle: 72 alw obsNotAt(robX, robY, obsX, obsY);