A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA. More...

Public Member Functions
	LTLfSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space)
	Construct an LtlfSynthesizer. More...

SynthesisResult	run () const
	Solves the LTLf synthesis problem. More...

std::unique_ptr< Transducer >	AbstractSingleStrategy (const SynthesisResult &result) const
	Abstract a winning strategy for the agent. More...

Detailed Description

A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA.

Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi: Symbolic LTLf Synthesis. IJCAI 2017: 1362-1369

Constructor & Destructor Documentation

Syft::LTLfSynthesizer::LTLfSynthesizer	(	SymbolicStateDfa	spec,
		Player	starting_player,
		Player	protagonist_player,
		CUDD::BDD	goal_states,
		CUDD::BDD	state_space
	)

Construct an LtlfSynthesizer.

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.

std::unique_ptr<Transducer> Syft::LTLfSynthesizer::AbstractSingleStrategy ( const SynthesisResult & result ) const

Abstract a winning strategy for the agent.

SynthesisResult Syft::LTLfSynthesizer::run ( ) const

Solves the LTLf synthesis problem.

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