Live Sequence Charts (LSCs) and related scenario-based notations enable requirements engineers to specify system behaviour in a way that is close to stakeholders’ narratives. However, when such scenario collections are translated to reactive synthesis problems (e.g. GR(1) games), they may turn out to be unrealizable: no system strategy can satisfy all mandatory scenarios against an unrestricted environment. Prior work has mostly reported unrealizability but has given limited support for repairing the specification. This paper proposes a method for assumption mining for scenario-based specifications: given an unrealizable scenario set, we extract from the counter-strategy of the environment the minimum behavioural commitments that the environment must respect so that the original scenario set becomes realizable. These commitments are then projected back to scenario form as additional LSCs (“environment scenarios”). Our approach proceeds in four steps: (1) translate the LSCs to a GR(1)-like game structure; (2) detect unrealizability and compute a winning environment counter-strategy; (3) generalize the counter-strategy into a set of liveness/safety assumptions over environment-controlled messages; (4) render those assumptions as LSCs that requirements engineers can read and negotiate. We illustrate the approach on a variation of the elevator-with-vent example—a typical case where fairness of the environment is missing—and show that the synthesized assumptions are small, comprehensible, and sufficient to restore realizability. The contribution is a bridge between formal counterexample information and the scenario language used by stakeholders.
Live Sequence Charts (LSCs) and related scenario-based notations enable requirements engineers to specify system behaviour in a way that is close to stakeholders’ narratives. However, when such scenario collections are translated to reactive synthesis problems (e.g. GR(1) games), they may turn out to be unrealizable: no system strategy can satisfy all mandatory scenarios against an unrestricted environment. Prior work has mostly reported unrealizability but has given limited support for repairing the specification. This paper proposes a method for assumption mining for scenario-based specifications: given an unrealizable scenario set, we extract from the counter-strategy of the environment the minimum behavioural commitments that the environment must respect so that the original scenario set becomes realizable. These commitments are then projected back to scenario form as additional LSCs (“environment scenarios”). Our approach proceeds in four steps: (1) translate the LSCs to a GR(1)-like game structure; (2) detect unrealizability and compute a winning environment counter-strategy; (3) generalize the counter-strategy into a set of liveness/safety assumptions over environment-controlled messages; (4) render those assumptions as LSCs that requirements engineers can read and negotiate. We illustrate the approach on a variation of the elevator-with-vent example—a typical case where fairness of the environment is missing—and show that the synthesized assumptions are small, comprehensible, and sufficient to restore realizability. The contribution is a bridge between formal counterexample information and the scenario language used by stakeholders.
