A maxset-synthesizer for a reachability game given as a symbolic-state DFA. More...

Public Member Functions
	LTLfMaxSetSynthesizer (SymbolicStateDfa spec, Player starting_player, Player protagonist_player, CUDD::BDD goal_states, CUDD::BDD state_space)
	Construct a MaxSet-LtlfSynthesizer. More...

MaxSetSynthesisResult	run () const
	Solves the MaxSet-LTLf synthesis problem. More...

void	dump_dot (MaxSetSynthesisResult maxset, const std::string &def_filename, const std::string &nondef_filename) const

Detailed Description

A maxset-synthesizer for a reachability game given as a symbolic-state DFA.

Shufang Zhu, Giuseppe De Giacomo: Synthesis of Maximally Permissive Strategies for LTLf Specifications. IJCAI 2022: 2783-2789

Constructor & Destructor Documentation

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

Construct a MaxSet-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.

MaxSetSynthesisResult Syft::LTLfMaxSetSynthesizer::run ( ) const

Solves the MaxSet-LTLf synthesis problem.

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