Receding horizon Temporal Logic Planning

Specification module

class spec.GRSpec(env_vars=[], sys_vars=[], env_init='', sys_init='', env_safety='', sys_safety='', env_prog='', sys_prog='')

GRSpec class for specifying a GR[1] specification of the form:

(env_init & []env_safety & []<>env_prog) -> (sys_init & []sys_safety & []<>sys_prog)

A GRSpec object contains the following fields:

• C{env_vars}: a list of variables (names given as strings) that are determined by the environment.
• C{env_init}: a string or a list of string that specifies the assumption about the initial state of the environment.
• C{env_safety}: a string or a list of string that specifies the assumption about the evolution of the environment state.
• C{env_prog}: a string or a list of string that specifies the justice assumption on the environment.
• C{sys_vars}: a list of variables (names given as strings) that are controlled by the system.
• C{sys_init}: a string or a list of string that specifies the requirement on the initial state of the system.
• C{sys_safety}: a string or a list of string that specifies the safety requirement.
• C{sys_prog}: a string or a list of string that specifies the progress requirement.

An empty list for any formula (e.g., if env_init = []) is marked as “True” in the specification. This corresponds to the constant Boolean function, which usually means that subformula has no effect (is non-restrictive) on the spec.

dumpgr1c()

Dump to gr1c specification string.

importDiscDynamics(disc_dynamics, cont_varname='cellID')

Append results of discretization (abstraction) to specification.

disc_dynamics is an instance of PropPreservingPartition, such as returned by the function discretize in module discretize.

• The cell names are not mangled, in contrast to the approach taken in the createProbFromDiscDynamics method of the SynthesisProb class.
• Any name in disc_dynamics.list_prop_symbol matching a system variable is removed from sys_vars, and its occurrences in the specification are replaced by a disjunction of corresponding cells.
• gr1c does not (yet) support variable domains beyond Boolean, so we treat each cell as a separate Boolean variable and explicitly enforce mutual exclusion.

importGridWorld(gworld, offset=(0, 0), controlled_dyn=True)

Append specification describing a gridworld.

Basically, call the spec method of the given GridWorld object and merge with its output. See documentation about the L{spec<gridworld.GridWorld.spec>} method of L{GridWorld<gridworld.GridWorld>} class for details.

@type gworld: L{GridWorld}

sym2prop(props, verbose=0)

Replace the symbols of propositions in this spec with the actual propositions

toJTLVSpec()

Return a list of two strings [assumption, guarantee] corresponding to this GR[1] specification.

Receding horizon Temporal Logic Planning Module

class rhtlp.RHTLPProb(shprobs=[], Phi='True', discretize=False, **args)

RHTLPProb class for specifying a receding horizon temporal logic planning problem.

A RHTLPProb object contains the following fields:

• shprobs: a list of ShortHorizonProb objects
• Phi: the invariant for the RHTLP problem

Constructor:

RHTLPProb ([ shprobs = [][, Phi = ‘True’[, discretize = False[, file = ‘’]]]]): construct this SynthesisProb object from file.

RHTLPProb ([ shprobs = [][, Phi = ‘True’[, discretize = False[, env_vars = {}[, ` sys_disc_vars` = {}[, disc_props = {}[, disc_dynamics = None[, spec = GRSpec()]]]]]]]])

RHTLPProb ([ shprobs = [][, Phi = ‘True’[, discretize = False[, env_vars = {}[, sys_disc_vars = {}[, disc_props = {}[, cont_state_space = None[, cont_props = {}[, sys_dyn = None[, spec = GRSpec()]]]]]]])

• shprobs: a list of ShortHorizonProb objects.
• Phi: a string specifying the invariant for the RHTLP problem.
• discretize: a boolean indicating whether to discretize the global problem.
• file: the name of the rhtlp file to be parsed. If file is given, the rest of the inputs to this function will be ignored.
• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• disc_dynamics: a PropPreservingPartition object that represents the transition system obtained from the discretization procedure. If disc_dynamics is given, cont_state_space, cont_props and sys_dyn will be ignored.
• cont_state_space: a Polytope object that represent the state space of the continuous variables. Needed only when discretize is True.
• cont_props: a dictionary {str : Polytope} whose keys are the symbols for propositions on continuous variables and whose values are polytopes that represent the region in the state space in which the corresponding proposition hold. If discretize is False, cont_props can be just a list of symbols for propositions on continuous variables.
• sys_dyn: a CtsSysDyn object that specifies the dynamics of the continuous variables. Needed only when discretize is True.
• spec: a GRSpec object that specifies the specification of this synthesis problem
• verbose: an integer that specifies the level of verbosity.

addSHProb(shprob)

Add a short horizon problem to this RHTLP problem.

checkTautologyPhi(verbose=0)

Check whether sys_init -> Phi is a tautology.

checkcovering(excluded_state=[], verbose=0)

Check whether the disjunction of all the W’s covers the entire state space.

computePhi(checktautology=True, verbose=0)

Compute Phi for this RHTLPProb object. Return a boolean that indicates whether a valid Phi exists.

constructWGraph(verbose=0)

Construct the graph for W’s. There is an edge in this graph from Wi to Wj if F(Wi) = Wj.

findW0Ind(verbose=0)

Find the indices of W0 in shprobs

getContProps()

Return copy of cont_props attribute.

getPhi()

Return the global invariant Phi for this RHTLP problem.

updatePhi(verbose=0)

Update Phi for this RHTLPProb object based on the local Phi in the short horizon problems.

validate(checkcovering=True, excluded_state=[], checkpartial_order=True, checktautology=True, checkrealizable=True, heap_size='-Xmx128m', verbose=0)

Check whether the list of ShortHorizonProb objects satisfies the sufficient conditions for receding horizon temporal logic planning.

class rhtlp.ShortHorizonProb(W='', FW=[], Phi='', global_prob=<rhtlp.SynthesisProb instance at 0x105ac4b90>, **args)

ShortHorizonProb class for specifying a short horizon problem for receding horizon temporal logic planning.

A ShortHorizonProb object contains the following fields:

• W: a proposition that specifies a set W of states.
• FW: a ShortHorizonProb object or a list of ShortHorizonProb object that specifies the set F(W).
• Phi: a proposition that specifies the receding horizon invariant.
• global_prob: a SynthesisProb object that represents the global problem.

Constructor:

ShortHorizonProb ([ W = ‘’[, FW = [][, Phi = ‘’[, global_prob = SynthesisProb()[, file = ‘’]]]]])

ShortHorizonProb ([ W = ‘’[, FW = [][, Phi = ‘’[, global_prob = SynthesisProb()[, env_vars = {}[, sys_disc_vars = {}[, disc_props = {}[, disc_dynamics = None]]]]]]]])

ShortHorizonProb ([ W = ‘’[, FW = [][, Phi = ‘’[, global_prob = SynthesisProb()[, env_vars = {}[, sys_disc_vars = {}[, disc_props = {}[, cont_state_space = None[, cont_props = {}[, sys_dyn = None]]]]]]]]]])

• W: a proposition that specifies a set W of states.
• FW: a ShortHorizonProb object or a list of ShortHorizonProb object that specifies the set F(W).
• Phi: a proposition that specifies the receding horizon invariant.
• global_spec: the global specification of the system.
• file: the name of the rhtlp file to be parsed. If file is given, the rest of the inputs to this function will be ignored.
• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• disc_dynamics: a PropPreservingPartition object that represents the transition system obtained from the discretization procedure. If disc_dynamics is given, cont_state_space, cont_props and sys_dyn will be ignored.
• cont_state_space: a Polytope object that represent the state space of the continuous variables. Needed only when discretize is True.
• cont_props: a dictionary {str : Polytope} whose keys are the symbols for propositions on continuous variables and whose values are polytopes that represent the region in the state space in which the corresponding proposition hold. If discretize is False, cont_props can be just a list of symbols for propositions on continuous variables.
• sys_dyn: a CtsSysDyn object that specifies the dynamics of the continuous variables. Needed only when discretize is True.
• verbose: an integer that specifies the level of verbosity.

computeLocalPhi(verbose=0)

Compute the local Phi for this ShortHorizonProb object. Return a boolean that indicates whether the local Phi gets updated. If the current prob is realizable, then the local Phi is not updated and this function will return False. Otherwise, the local Phi will get updated and this function wil return True.

getFW()

Return the set F(W) of this short horizon problem.

getGlobalSpec()

Return the global specification of this short horizon problem.

getLocalPhi(allow_disc_cont_var=True)

Return the local invariant Phi of this short horizon problem.

getW()

Return the set W of this short horizon problem.

setFW(FW, update=True, verbose=0)

Set the set F(W) of this short horizon problem.

setLocalPhi(Phi, update=True, verbose=0)

Set the local invariant Phi of this short horizon problem.

setW(W, update=True, verbose=0)

Set the set W of this short horizon problem.

updateLocalSpec(verbose=0)

Update the short horizon specification based on the current W, FW and Phi.

class rhtlp.SynthesisProb(**args)

SynthesisProb class for specifying a planner synthesis problem.

A SynthesisProb object contains the following fields:

• env_vars: a dictionary {str : str} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, 3, 4, 5}.
• sys_vars: a dictionary {str : str} whose keys are the names of system variables and whose values are their possible values.
• spec: a GRSpec object that specifies the specification of this synthesis problem.
• disc_cont_var: the name of the continuous variable after the discretization.
• disc_dynamics: a list of Region objects corresponding to the partition of the continuous state space.

Constructor:

SynthesisProb ([ file = ‘’[, verbose = 0]]): construct this SynthesisProb object from file

• file: the name of the rhtlp file to be parsed. If file is given, the rest of the inputs to this function will be ignored.

SynthesisProb ([ env_vars = {}[, sys_disc_vars = {}[, disc_props = {}[, disc_dynamics = None[, spec = GRSpec()[, verbose = 0]]]]]])

SynthesisProb ([ env_vars = {}[, sys_disc_vars = {}[, disc_props = {}[, cont_state_space = None[, cont_props = {}[, sys_dyn = None[, spec = GRSpec()[, verbose = 0]]]]]]]])

• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• disc_dynamics: a PropPreservingPartition object that represents the transition system obtained from the discretization procedure. If disc_dynamics is given, cont_state_space, cont_props and sys_dyn will be ignored.
• cont_state_space: a Polytope object that represent the state space of the continuous variables
• cont_props: a dictionary {str : Polytope} whose keys are the symbols for propositions on continuous variables and whose values are polytopes that represent the region in the state space in which the corresponding proposition hold.
• sys_dyn: a CtsSysDyn object that specifies the dynamics of the continuous variables
• spec: a GRSpec object that specifies the specification of this synthesis problem
• verbose: an integer that specifies the level of verbosity.

checkRealizability(heap_size='-Xmx128m', pick_sys_init=True, verbose=0)

Determine whether this SynthesisProb is realizable without extracting an automaton.

Input:

• heap_size: a string that specifies java heap size.
• pick_sys_init is a boolean indicating whether the system can pick its initial state (in response to the initial environment state).
• verbose: an integer that specifies the level of verbosity.

createProbFromContDynamics(env_vars={}, sys_disc_vars={}, disc_props={}, cont_state_space=None, cont_props={}, sys_dyn=None, spec=<spec.GRSpec instance at 0x105ac4878>, verbose=0)

Construct SynthesisProb from continuous dynamics.

Input:

• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• cont_state_space: a Polytope object that represent the state space of the continuous variables
• cont_props: a dictionary {str : Polytope} whose keys are the symbols for propositions on continuous variables and whose values are polytopes that represent the region in the state space in which the corresponding proposition hold.
• sys_dyn: a CtsSysDyn object that specifies the dynamics of the continuous variables
• spec: a GRSpec object that specifies the specification of this synthesis problem.
• verbose: an integer that specifies the level of verbosity.

createProbFromDiscDynamics(env_vars={}, sys_disc_vars={}, disc_props={}, disc_dynamics=<prop2part.PropPreservingPartition instance at 0x105ac4950>, spec=None, verbose=0)

Construct SynthesisProb from discretized continuous dynamics.

Input:

• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• disc_dynamics: a PropPreservingPartition object that represents the transition system obtained from the discretization procedure.
• spec: a GRSpec object that specifies the specification of this synthesis problem.
• verbose: an integer that specifies the level of verbosity.

getCounterExamples(recompute=False, heap_size='-Xmx128m', pick_sys_init=True, verbose=0)

Return a list of dictionary representing a state starting from which the system cannot satisfy the spec.

getDiscProps()

Return the discrete propositions as a dictionary whose key is the symbol of the proposition and whose value is the actual formula of the proposition.

getDiscretizedContVar()

Return the name of the discretized continuous variable.

getDiscretizedDynamics()

Return the discretized dynamics.

getEnvVars()

Return the environment variables of this object as a dictionary whose key is the name of the variable and whose value is the possible values that the variable can take.

getJTLVFile()

Return the name of JTLV files. The smv, spc and aut files are appended by .smv, .spc and .aut, respectively.

getSpec()

Return the specification of this object.

getSysDiscVars()

Return the system discrete variables of this object as a dictionary whose key is the name of the variable and whose value is the possible values that the variable can take.

getSysVars()

Return the system (discrete and discretized continuous) variables of this object as a dictionary whose key is the name of the variable and whose value is the possible values that the variable can take.

getYsFile()

Return the name of the (temporary) Yices file.

setDiscProps(disc_props, verbose=0)

Set the propositions on discrete variables.

setDiscretizedDynamics(disc_dynamics, verbose=0)

Set the discretized dynamics.

setEnvVars(env_vars, verbose=0)

Set the environment variables.

setJTLVFile(jtlvfile)

Set the temporary jtlv files (smv, spc, aut).

setSpec(spec, verbose=0)

Set the specification.

setSysDiscVars(sys_disc_vars, verbose=0)

Set the system discrete variables.

setYsFile(ysfile)

Set the temporary Yices file (*.ys).

synthesizePlannerAut(heap_size='-Xmx128m', priority_kind=3, init_option=1, verbose=0)

Compute a planner automaton for this SynthesisProb.

If this SynthesisProb is realizable, this function returns an Automaton object. Otherwise, it returns a list of dictionary that represents the state starting from which there exists no strategy for the system to satisfy the spec.

Input:

• heap_size: a string that specifies java heap size.
• priority_kind: a string of length 3 or an integer that specifies the type of priority used in extracting the automaton. See the documentation of the computeStrategy function for the possible values of priority_kind.
• init_option: an integer in that specifies how to handle the initial state of the system. See the documentation of the computeStrategy function for the possible values of init_option.
• verbose: an integer that specifies the level of verbosity. If verbose is set to 0, this function will not print anything on the screen.

toJTLVInput(smv_file='', spc_file='', file_exist_option='r', verbose=0)

Generate JTLV input files: smv_file and spc_file for this SynthesisProb.

Input:

• smv_file: a string that specifies the name of the resulting smv file.
• spc_file: a string that specifies the name of the resulting spc file.
• file_exist_option: a string that indicate what to do when the specified smv_file or spc_file exists. Possible values are: ‘a’ (ask whether to replace or create a new file), ‘r’ (replace the existing file), ‘n’ (create a new file).
• verbose: an integer that specifies the level of verbosity. If verbose is set to 0, this function will not print anything on the screen.