Syft::StabilityLtlfSynthesizer Class Reference

A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Stability assumption. The simple Stability assumption is in the form of FG\alpha, where \alpha is a Boolean formula over environment variables. More...

#include <StabilityLtlfSynthesizer.h>

Public Member Functions
	StabilityLtlfSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space, const std::string &assumption_filename)
	Construct an StabilityLtlfSynthesizer. More...
SynthesisResult	run () const
	Solves the synthesis problem of LTLf with simple Stability environment assumption. More...

Protected Member Functions
CUDD::BDD	load_CNF (const std::string &filename) const

Detailed Description

A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA, considering environment simple Stability assumption. The simple Stability assumption is in the form of FG\alpha, where \alpha is a Boolean formula over environment variables.

Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi: LTLƒ Synthesis with Fairness and Stability Assumptions. AAAI 2020: 3088-3095

Constructor & Destructor Documentation

StabilityLtlfSynthesizer()

Syft::StabilityLtlfSynthesizer::StabilityLtlfSynthesizer	(	SymbolicStateDfa	spec,
		Player	starting_player,
		Player	protagonist_player,
		CUDD::BDD	goal_states,
		CUDD::BDD	state_space,
		const std::string &	assumption_filename
	)

Construct an StabilityLtlfSynthesizer.

Parameters

spec	A symbolic-state DFA representing the LTLf formula.
starting_player	The player that moves first each turn.
protagonist_player	The player for which we aim to find the winning strategy.
goal_states	The set of states that the agent must reach to win.
state_space	The state space.
assumption_filename	The file that specifies a Boolean formula \alpha over input variables, denoting the simple Stability assumption FG\alpha.

Member Function Documentation

run()

SynthesisResult Syft::StabilityLtlfSynthesizer::run

(

)

const

Solves the synthesis problem of LTLf with simple Stability environment assumption.

Returns

The synthesis result.

---

The documentation for this class was generated from the following files:

• src/synthesis/header/synthesizer/StabilityLtlfSynthesizer.h
• src/synthesis/source/synthesizer/StabilityLtlfSynthesizer.cpp