Method and system for mission planning via formal verification and supervisory controller synthesis
First Claim
1. A method implemented by a computing system in response to execution of program instructions by a processor of the computing system, the method comprising:
- receiving, by at least one decomposition module of a mission planning module, a set of formalized requirements generated by a requirements formalization engine for accomplishing a mission;
allocating, by a processor of the decomposition module, using architecture synthesis, constraint solving, and compositional verification techniques, a role to each of a plurality of assets comprising a team of autonomous entities responsible to accomplish the mission, each of the plurality of assets of the team to execute specific tasks according to their allocated role to accomplish the mission;
generating, by a processor of at least one supervisory controller synthesis module using controller synthesis and formal verification techniques, automatically and in response to the set of formalized requirements and the roles allocated to the plurality of assets, a mission plan for accomplishing the mission by the plurality of assets, the mission plan being generated to automatically and dynamically react to external inputs during a run-time execution of the mission plan by the plurality of assets to execute tasks according to their allocated role to accomplish the mission plan;
sending the generated mission plan to the plurality of assets for the plurality of assets to, during a run-time execution of the mission plan, execute tasks in reaction to the external inputs and according to their allocated role to accomplish the mission;
wherein the method further comprises generating a plurality of contracts between the plurality of assets, where the plurality of contracts represents obligations the plurality of assets has with each other and the coordination required to fulfill those obligations; and
wherein the breaking or breaching of at least one contract among the plurality of contracts triggers a change in mission templates to be executed by the plurality of assets.
1 Assignment
0 Petitions
Accused Products
Abstract
A system, medium, and method, including receiving a set of formalized requirements for accomplishing a mission; allocating, by the processor using architecture synthesis, constraint solving, and compositional verification techniques, a role to each of a plurality of assets comprising a team of autonomous entities, the team to execute specific tasks according to their role to accomplish the mission; and generating, by the processor using controller synthesis and verification techniques, automata for accomplishing the mission for the plurality of assets, the automata being encoded to confer an ability to dynamically react to external inputs during a run-time execution of the automata by the plurality of assets.
45 Citations
22 Claims
-
1. A method implemented by a computing system in response to execution of program instructions by a processor of the computing system, the method comprising:
-
receiving, by at least one decomposition module of a mission planning module, a set of formalized requirements generated by a requirements formalization engine for accomplishing a mission; allocating, by a processor of the decomposition module, using architecture synthesis, constraint solving, and compositional verification techniques, a role to each of a plurality of assets comprising a team of autonomous entities responsible to accomplish the mission, each of the plurality of assets of the team to execute specific tasks according to their allocated role to accomplish the mission; generating, by a processor of at least one supervisory controller synthesis module using controller synthesis and formal verification techniques, automatically and in response to the set of formalized requirements and the roles allocated to the plurality of assets, a mission plan for accomplishing the mission by the plurality of assets, the mission plan being generated to automatically and dynamically react to external inputs during a run-time execution of the mission plan by the plurality of assets to execute tasks according to their allocated role to accomplish the mission plan; sending the generated mission plan to the plurality of assets for the plurality of assets to, during a run-time execution of the mission plan, execute tasks in reaction to the external inputs and according to their allocated role to accomplish the mission; wherein the method further comprises generating a plurality of contracts between the plurality of assets, where the plurality of contracts represents obligations the plurality of assets has with each other and the coordination required to fulfill those obligations; and wherein the breaking or breaching of at least one contract among the plurality of contracts triggers a change in mission templates to be executed by the plurality of assets. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8)
-
-
9. A system comprising:
-
at least one decomposition module of a mission planning module to; receive a set of formalized requirements generated by a requirements formalization engine for accomplishing a mission; and allocate, by a processor of the decomposition module, using architecture synthesis, constraint solving, and compositional verification techniques, a role to each of a plurality of assets comprising a team of autonomous entities to be responsible of accomplishing the mission, each of the plurality of assets of the team to execute specific tasks according to their allocated role to accomplish the mission; and at least one supervisory controller synthesis module to; automatically generate by a processor thereof using controller synthesis and formal verification techniques in response to the set of formalized requirements and the roles allocated to the plurality of assets, a mission plan for accomplishing the mission by the plurality of assets according to their allocated role to accomplish the mission plan, the mission plan being generated to automatically and dynamically react to external inputs during a run-time execution of the mission plan by the plurality of assets; send the generated mission plan to the plurality of assets for the plurality of assets to, during a run-time execution of the mission plan, execute tasks in reaction to the external inputs and according to their allocated role to accomplish the mission; wherein the decomposition module generates a plurality of contracts between the plurality of assets, where the plurality of contracts represents obligations the plurality of assets has with each other and the coordination required to fulfill those obligations; and wherein the breaking or breaching of at least one contract among the plurality of contracts triggers a change in mission templates to be executed by the plurality of assets. - View Dependent Claims (10, 11, 12, 13, 14, 15, 16)
-
-
17. A non-transitory, computer-readable medium storing instructions thereon, the medium comprising:
-
program instructions to receive, by at least one decomposition module of a mission planning module, a set of formalized requirements generated by a requirements formulization engine for accomplishing a mission; program instructions to allocate, by a processor of the decomposition module, using architecture synthesis, constraint solving, and compositional verification techniques, a role to each of a plurality of assets comprising a team of autonomous entities to be responsible of accomplishing the mission, each of the plurality of assets of the team to execute specific tasks according to their role to accomplish the mission; and program instructions to generate, by a processor of at least one supervisory controller synthesis module using controller synthesis and formal verification techniques automatically and in response to the set of formalized requirements and the roles allocated to the plurality of assets, a mission plan for accomplishing the mission by the plurality of assets, the mission plan being generated to automatically and dynamically react to external inputs during a run-time execution of the mission plan by the plurality of assets to execute tasks according to their role to accomplish the mission plan; program instructions to send the generated mission plan to the plurality of assets for the plurality of assets to, during a run-time execution of the mission plan, execute tasks in reaction to the external inputs and according to their allocated role to accomplish the mission; wherein the medium further comprises program instructions to generate a plurality of contracts between the plurality of assets, where the plurality of contracts represents obligations the plurality of assets has with each other and the coordination required to fulfill those obligations; and wherein the breaking or breaching of at least one contract among the plurality of contracts triggers a change in mission templates to be executed by the plurality of assets. - View Dependent Claims (18, 19, 20, 21, 22)
-
Specification