Syft::FairnessLtlfSynthesizer Class Reference

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

#include <FairnessLtlfSynthesizer.h>

Public Member Functions
	FairnessLtlfSynthesizer (const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space, const std::string &assumption_filename)
	Construct a FairnessLtlfSynthesizer. More...
SynthesisResult	run () const
	Solves the synthesis problem of LTLf with simple Fairness 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 Fairness assumption. The simple Fairness assumption is in the form of GF\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

FairnessLtlfSynthesizer()

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

Construct a FairnessLtlfSynthesizer.

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 Fairness assumption GF\alpha.

Member Function Documentation

run()

SynthesisResult Syft::FairnessLtlfSynthesizer::run

(

)

const

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

Returns

The synthesis result.

---

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

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