DETAILED ACTION
Notice of Pre-AIA or AIA Status
The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
This office action is in response to Applicant’s communication filed on 09/30/2024. Claims 1-20 have been examined.
Information Disclosure Statement
The information disclosure statement(IDS) submitted on 10/13/2025. The submission is in compliance with the provisions of 37 CFR 1.97. Accordingly, the information disclosure statement is being considered by the examiner.
Claim Objections
Claim 20 is objected to because of the following informalities:
With regards to claim 20, the claim recites “ by a processor of a computer causes a computer …”. Examiner suggests amending the claim to recites : “by a processor of a computer causes the computer …” Appropriate correction is required.
Claim Rejections - 35 USC § 101
35 U.S.C. 101 reads as follows:
Whoever invents or discovers any new and useful process, machine, manufacture, or composition of matter, or any new and useful improvement thereof, may obtain a patent therefor, subject to the conditions and requirements of this title.
Claims 1-20 are rejected under 35 U.S.C. 101 because the claimed invention is directed to an abstract idea without significantly more.
The claims 1, 11, 20 recite “ (1) receiving an input and output example; (2) generating using the input and output example and synthesis algorithm, a logical specification defining network protocol … (3) outputting the logical specification.
The limitations of (2) generating , (3) outputting as drafted are processes that under their broadest reasonable interpretation , cover performance of the limitations which can be practically performed in the human mind. These limitations encompass mental observation and evaluations ( e.g. computer programmer’s observing the data, making a determination and evaluation , and outputting the result). Thus, These limitations recite a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
The (1) receiving limitation represents mere data gathering. This limitation does not impose any meaningful limits on the claims. The limitation amounts to necessary data gathering.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims 1,20 only recite additional elements–“system comprising: a processor; and a memory; and a network specification synthesizer (NSS) implemented using the processor and the memory,,” .”non transitory computer medium… by a processor of computer”
The additional elements as shown above recite at a high-level of generality such that it amounts no more than mere instructions to apply the exception using a generic computer components.
Accordingly, these additional elements do not integrate the abstract idea into a practical application because they do not impose any meaningful limits on practicing the abstract idea. The claims are directed to an abstract idea.
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 2,12, the claims recite the limitations: 1) detecting incompleteness in the input and output examples…. 2) generating a supplemental input example …. 3) requesting and receiving .. supplemental output …. and 4) utilizing the supplemental input and output examples in generating logical specification.
The limitations of (1) detecting , (2) generating , 4) utilizing as drafted are processes that under their broadest reasonable interpretation , cover performance of the limitations which can be practically performed in the human mind. These limitations encompass mental observation and evaluations ( e.g. computer programmer’s observing the data, generating a supplemental input, and using the supplemental input to generate data). Thus, These limitations recite a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
The (3) receiving/requesting limitation represents mere data gathering. This limitation does not impose any meaningful limits on the claims. The limitation amounts to necessary data gathering.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 3,13, the claims recite the limitation: 1) wherein the synthesis algorithm utilizes a best-first search algorithm that incrementally explores an unbounded search ….
The limitation of utilizing as drafted is process that under its broadest reasonable interpretation , covers performance of the limitation which can be practically performed in the human mind. This limitation encompasses mental observation and evaluations ( e.g. computer programmer’s observing the data, utilizing a search , and outputting the result). Thus, This limitation recites a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 4,14, the claims recite the limitations: 1) performing iteration loop …. 2) mutating using at least one mutation strategy , a first candidate specification… to generate a plurality of offspring candidates, wherein the plurality of offspring candidates are scored 3) selecting … and using scores of the plurality of offspring candidates a second candidate specification to mutate.
The limitations of 1) performing, 2) mutating , 3) selecting as drafted are processes that under their broadest reasonable interpretation , cover performance of the limitations which can be practically performed in the human mind. These limitations encompass mental observation and evaluations ( e.g. computer programmer’s observing the data, modifying the data based on strategy, scoring and selecting candidates using the scoring ). Thus, These limitations recite a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 5,16, the claims recite the limitation: 1) wherein the second candidate specification to mutate is selected from offspring candidates that have higher scores…
The limitation of 1) selecting as drafted is process that under its broadest reasonable interpretation , covers performance of the limitation which can be practically performed in the human mind. This limitation encompasses mental observation and evaluations ( e.g. computer programmer’s observing the data, scoring and selecting candidates with higher scores ). Thus, These limitation recites a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 6,15, the claims recite the limitation: 1) wherein the at least one mutation strategy including adding the rule…
The limitation of 1) adding as drafted is process that under its broadest reasonable interpretation , covers performance of the limitation which can be practically performed in the human mind. This limitation encompasses mental observation and evaluations ( e.g. computer programmer’s modifying the data based on adding the rule ). Thus, This limitation recites a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 7,17, the claims recite the limitation: 1) wherein the input and output examples include a first input example and a first output example, wherein the first input example includes network information, topology information, virtual machine (VM) configuration information, link cost information, or a weighted directed graph and the first output example includes network state information, shortest or best path information, or reachable VM pair information… “ the claim limitation only defines what the input and output examples are.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claim 8 the claim recites the limitation: 1) utilizing traces or monitoring of runtime executions of the network protocol to obtain or derive the input and output examples… “
The limitation of 1) utilizing as drafted is process that under its broadest reasonable interpretation , covers performance of the limitation which can be practically performed in the human mind. This limitation encompasses mental observation and evaluations ( e.g. computer programmer’s utilizing traces to derive input and output example ). Thus, This limitation recites a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claim 8 only recite additional elements–“a network specification synthesizer (NSS) ”
The additional element as shown above recites at a high-level of generality such that it amounts no more than mere instructions to apply the exception using a generic computer components.
Accordingly, this additional element does not integrate the abstract idea into a practical application because they do not impose any meaningful limits on practicing the abstract idea. The claim is directed to an abstract idea.
The claim does not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional element amounts to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claim is not patent eligible.
With regards to claims 9,18 the claims recite the limitations: 1) using the logical specification for verification, analysis, or prototyping purposes.… “
The limitation of 1) using as drafted is process that under its broadest reasonable interpretation , covers performance of the limitations which can be practically performed in the human mind. This limitation encompasses mental observation and evaluations ( e.g. computer programmer’s observing the data, evaluating the data and making determination ). Thus, This limitation recites a concept that falls into the “mental process group” , “a method of organizing human activity group” of abstract ideas.
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claim 9 only recite additional elements–“a network specification synthesizer (NSS) ”
The additional element as shown above recites at a high-level of generality such that it amounts no more than mere instructions to apply the exception using a generic computer components.
Accordingly, this additional element does not integrate the abstract idea into a practical application because they do not impose any meaningful limits on practicing the abstract idea. The claim is directed to an abstract idea.
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional element amounts to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
With regards to claims 10,19 the claims recite the limitations: 1) wherein the logical specification is expressed using a declarative logic programming language, Datalog, or an extended Datalog like language..… “ the claim limitation only defines what type of language the logical specification is using .
Therefore, the claims are directed to an abstract idea.
This judicial exception is not integrated into a practical application. In particular, the claims do no recite additional elements
The claims do not include additional elements that are sufficient to amount to significantly more than the judicial exception. As discussed above with respect to integration of the abstract idea into a practical application, the additional elements amount to no more than mere instructions to apply the exception using a generic computer component. Mere instructions to apply an exception using a generic computer component cannot provide an inventive concept. The claims are not patent eligible.
Claim Rejections - 35 USC § 112
The following is a quotation of 35 U.S.C. 112(b):
(b) CONCLUSION.—The specification shall conclude with one or more claims particularly pointing out and distinctly claiming the subject matter which the inventor or a joint inventor regards as the invention.
The following is a quotation of 35 U.S.C. 112 (pre-AIA ), second paragraph:
The specification shall conclude with one or more claims particularly pointing out and distinctly claiming the subject matter which the applicant regards as his invention.
Claims 1 – 19 are rejected under 35 U.S.C. 112(b) or 35 U.S.C. 112 (pre-AIA ), second paragraph, as being indefinite for failing to particularly point out and distinctly claim the subject matter which the inventor or a joint inventor (or for applications subject to pre-AIA 35 U.S.C. 112, the applicant), regards as the invention.
With regards to claims 1,2, 7, 8, 11,12,17, the claims recite “ the input and output examples”. It is unclear what the input and output examples are referring to because the claims 1,11 recite “ input and output examples” in the preamble and “input and output examples” in the receiving limitation. Therefore, the examiner is unable to determine the metes and bounds of the claim language.
Claim Rejections - 35 USC § 102
The following is a quotation of the appropriate paragraphs of 35 U.S.C. 102 that form the basis for the rejections under this section made in this Office action:
A person shall be entitled to a patent unless –
(a)(1) the claimed invention was patented, described in a printed publication, or in public use, on sale, or otherwise available to the public before the effective filing date of the claimed invention.
Claims 1,2,7-9,11,12,17,18,20 are rejected under 35 U.S.C. 102 (a1) as being anticipated by Udupa et al. “ Synthesis of Distributed Protocols from scenarios and specifications” Publication date – 2016 ( Udupa hereinafter).
Regarding claim 1,
Udupa teaches a system for synthesizing network specifications using input and output examples (Abstract), the system comprising:
a processor; and a memory; and a network specification synthesizer (NSS) implemented using the processor and the memory, wherein the NSS is configured for receiving input and output examples associated with a network protocol; (Section 1 - The role of the synthesizer is to complete the incomplete protocol provided by the programmer, such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior - These unknown functions could be used in the guards for transitions which describe the condition under which the transition in question can be executed and the update functions to state variables on transitions which describe how the state variables of the state machine evolve upon execution of the transition. The programmer could also provide some information on the missing behavior. This information might be in the form of input-output examples describing the behavior of the unknown functions, or could be information about exactly what behavior is left unspecified; To construct a protocol from the concolic snippets provided by the programmer, transit needs to synthesize expressions which are consistent with each of the snippets provided by the programmer. Let us, for the moment, assume that constraints implied by the programmer in the concolic snippets can be translated precisely into a constraint , of the form described in Section 4.1. We will return to the question of how this translation is accomplished towards the end of this section. For the purpose of the synthesis algorithm, we treat the constraints obtained from both concrete and concolic snippets in the same way, i.e., as symbolic constraints over the expressions to be synthesized. For each unknown function – See ALSO Section 6.3.4)
generating, using the input and output examples and a synthesis algorithm, a logical specification defining the network protocol, wherein the logical specification includes a set of rules; and ( Section 1 – Introduction - In our formalization of the synthesis problem, processes communicate using input/output channels that carry typed messages. Each process is described by a state machine with a set of typed state variables. Transitions consist of guards — that test some condition over the state variables — and updates to state variables and fields of messages to be sent. Such guards and updates can involve unknown (typed) functions to be filled in by the synthesizer Section 8.1 - We model the unknown functions used in the guards and updates in the esm-sks as uninterpreted functions — rather than as Boolean variables as was the case in the algorithm described in Chapter 7 — and ask the SMT solver for an interpretation which satisfies the set of constraints maintained by the algorithm - See Algorithm 6.5, Section 6.3.3 - the algorithm eusolve, shown as Algorithm 6.5, shows how the Term Solve and Unify Terms algorithms are composed to form a complete SyGuS solver. The algorithm maintains a list of valuations P, which are built up from counterexamples returned by the algorithm Unify Terms. It repeatedly calls the algorithm Term Solve, followed by the algorithm Unify Terms, augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification - See Also Section 4.3);
outputting the logical specification (Section 1 - The role of the synthesizer is to complete the incomplete protocol provided by the programmer such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior. This methodology for protocol specification can be viewed as a fruitful collaboration between the designer and the synthesis tool: the programmer has to describe the structure of the desired protocol, but some details that the programmer is unsure about, for instance, regarding corner cases and handling of unexpected messages, are filled in automatically by the tool –Section 1.1 - This process often requires the programmer to reason globally about the protocol to avoid introducing new errors as in the corrected version of the protocol. This tedious process of discovering bugs and correcting the protocol is iterated until a correct protocol is constructed. We now illustrate this process with a concrete example of how a simple cache coherence protocol might be constructed using this methodology).
Regarding claim 2,
Udupa teaches
wherein the synthesis algorithm comprises: detecting incompleteness in the input and output examples used in generating the logical specification (Fig.1.1,& Fig.4.1; Section 1.1 - The resulting implementation is then checked for correctness using some combination of verification and testing techniques. For example, testing techniques could be used to check for correct behavior with respect to different scenarios specified by the programmer, whereas verification techniques could check that the candidate protocol satisfies the high-level safety and liveness specifications set forth by the programmer. In the event that an error is found during this check for correctness, the verification or testing framework provides the programmer with a concrete execution of the candidate protocol that demonstrates the error);
generating a supplemental input example usable for generating the logical specification, requesting and receiving, from a user, a supplemental output example corresponding to the supplemental input example (Fig 4.3 -Section 1.1 - the verification or testing framework provides the programmer with a concrete execution of the candidate protocol that demonstrates the error. The programmer then uses this information to refine or correct the behavior of the candidate protocol in the context of the specific counterexample currently under consideration. This process often requires the programmer to reason globally about the protocol to avoid introducing new errors as in the corrected version of the protocol – Section 4.2 - transit allows the programmer to fuse a transition involving the receipt of a message with a transition involving transmitting an output message, i.e., an input or internal transition, followed immediately by an output transition - An attempt to verify the protocol instantiated with this update, results in a violation of the coherence invariant. A visual representation of a simplified version of the error trace is shown in Figure 4.3. Observe that the transition shown on the directory esm in Figure 4.3 is a concrete instance of the concolic snippet that we have described, with the cache esm C2 being Msg.Sender and the Owner variable of the directory esm Dir initially set to C1. Upon inspecting the error trace, the programmer recognized that in this particular case, the new value of the Sharers variable needed to include the previous value of the Owner variable as well. The programmer codifies this using the following concrete snippet Fig.4.1, the one counterexample. transit integrates the new (concrete) constraints with the rest of the constraints to provide a new interpretation I which satisfies all the constraints. The protocol is instantiated with the new interpretation, and the process is repeated until a correct protocol is found. The programmer is thus freed from reasoning about the global properties of the protocol when handling corner-case behavior, which were not handled in the initial version of the protocol);
utilizing the supplemental input and output examples in generating the logical specification (Fig. 4.1, Section 4.1 - The programmer can then codify the fixes to any counterexamples obtained during this check using concrete input-output examples that correspond to a local fix, which eliminates at least the one counterexample transit integrates the new (concrete) constraints with the rest of the constraints to provide a new interpretation I which satisfies all the constraints. The protocol is instantiated with the new interpretation, and the process is repeated until a correct protocol is found – Section 6.3.3 - augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification).
Regarding claim 7,
Udupa further teaches
wherein the input and output examples include a first input example and a first output example, wherein the first input example includes network information, topology information, virtual machine (VM) configuration information, link cost information, or a weighted directed graph and the first output example includes network state information, shortest or best path information, or reachable VM pair information (Section 2.1 - We allow the developer to specify a skeleton or sketch of the protocol that defines (i) the set of communicating processes that make up the protocol (ii) the state variables of each communicating process that is part of the protocol, (iii) the communication architecture of the protocol, which defines which processes can communicate, and along which direction, as well as describes the properties of communication links between processes- Section 1.1.1 - The working of the VI coherence protocol is perhaps best explained using the scenarios shown in Figure 1.3. The protocol consists of two classes of state machines: The cache controller state machines, whose behaviors are symmetric, denoted by C1, C2, . . . , Cn in Figure 1.3, and a singular directory state machine, denoted by D in Figure 1.3. Each cache machine has a state variable named cdata which contains the cached value of data at any point, and can be undefined if the cache does not have an up-do-date cached copy of the data).
Regarding claim 8,
Udupa further teaches
wherein the NSS is configured for utilizing traces or monitoring of runtime executions of the network protocol to obtain or derive the input and output examples (Fig. 1.1 & Fig.3.2, Section 3.6 - Once a suitable interpretation I has been generated, the protocol is instantiated with this interpretation by the block labeled 6 , and checked for correctness against the user specified safety and liveness monitors ( 3 ) by the block labeled 7 . This check is performed using a model-checker. If the protocol is found to satisfy all the safety and liveness requirements, then the algorithm terminates with a success. On the other hand, if the model-checker discovers errors, these errors are used to generate additional constraints ( 8 ) which are then added to '. These additional constraints rule out at least the current interpretation I from being generated again – Section 4.1 - it is then checked for correctness. The programmer can then codify the fixes to any counterexamples obtained during this check using concrete input-output examples that correspond to a local fix, which eliminates at least the one counterexample - Figure 4.3: An error trace generated by the model checker in response to an incorrect completion for the SGI-Origin protocol synthesized by transit. – See Also Section 8.2.3).
Regarding claim 9,
Udupa further teaches
wherein the NSS is configured for using the logical specification for verification, analysis, or prototyping purposes; or wherein the NSS is configured for executing, using a compiler or interpreter, the logical specification and monitoring the execution of the logical specification for issues (Abstract - The programmer also specifies a set of high-level formal requirements that a correct protocol is expected to satisfy. These requirements can include safety requirements as well as liveness requirements in the form of Linear Temporal Logic formulas. We describe techniques to synthesize a correct protocol which is consistent with the common-case behavior specified by the programmer and also satisfies the high-level safety and liveness requirements set forth by the programmer – Section 1 - The programmer would also have to state the high-level correctness requirements for the protocol in a temporal logic of choice.1 The role of the synthesizer is to complete the incomplete protocol provided by the programmer, such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior – Section 1.1 - The resulting implementation is then checked for correctness using some combination of verification and testing techniques. For example, testing techniques could be used to check for correct behavior with respect to different scenarios specified by the programmer, whereas verification techniques could check that the candidate protocol satisfies the high-level safety and liveness specifications set forth by the programmer. In the event that an error is found during this check for correctness, the verification or testing framework provides the programmer with a concrete execution of the candidate protocol that demonstrates the error).
Regarding claim 11,
Udupa teaches a method for synthesizing network specifications using input and output examples, (Abstract), the method comprising:
receiving input and output examples associated with a network protocol; (Section 1 - The role of the synthesizer is to complete the incomplete protocol provided by the programmer, such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior - These unknown functions could be used in the guards for transitions which describe the condition under which the transition in question can be executed and the update functions to state variables on transitions which describe how the state variables of the state machine evolve upon execution of the transition. The programmer could also provide some information on the missing behavior. This information might be in the form of input-output examples describing the behavior of the unknown functions, or could be information about exactly what behavior is left unspecified; To construct a protocol from the concolic snippets provided by the programmer, transit needs to synthesize expressions which are consistent with each of the snippets provided by the programmer. Let us, for the moment, assume that constraints implied by the programmer in the concolic snippets can be translated precisely into a constraint , of the form described in Section 4.1. We will return to the question of how this translation is accomplished towards the end of this section. For the purpose of the synthesis algorithm, we treat the constraints obtained from both concrete and concolic snippets in the same way, i.e., as symbolic constraints over the expressions to be synthesized. For each unknown function);
generating, using the input and output examples and a synthesis algorithm, a logical specification defining the network protocol, wherein the logical specification includes a set of rules; ( Section 1 – Introduction - In our formalization of the synthesis problem, processes communicate using input/output channels that carry typed messages. Each process is described by a state machine with a set of typed state variables. Transitions consist of guards — that test some condition over the state variables — and updates to state variables and fields of messages to be sent. Such guards and updates can involve unknown (typed) functions to be filled in by the synthesizer Section 8.1 - We model the unknown functions used in the guards and updates in the esm-sks as uninterpreted functions — rather than as Boolean variables as was the case in the algorithm described in Chapter 7 — and ask the SMT solver for an interpretation which satisfies the set of constraints maintained by the algorithm - See Algorithm 6.5, Section 6.3.3 - the algorithm eusolve, shown as Algorithm 6.5, shows how the Term Solve and Unify Terms algorithms are composed to form a complete SyGuS solver. The algorithm maintains a list of valuations P, which are built up from counterexamples returned by the algorithm Unify Terms. It repeatedly calls the algorithm Term Solve, followed by the algorithm Unify Terms, augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification - See Also Section 4..3);
outputting the logical specification (Section 1 - The role of the synthesizer is to complete the incomplete protocol provided by the programmer such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior. This methodology for protocol specification can be viewed as a fruitful collaboration between the designer and the synthesis tool: the programmer has to describe the structure of the desired protocol, but some details that the programmer is unsure about, for instance, regarding corner cases and handling of unexpected messages, are filled in automatically by the tool – Section 1.1 - This process often requires the programmer to reason globally about the protocol to avoid introducing new errors as in the corrected version of the protocol. This tedious process of discovering bugs and correcting the protocol is iterated until a correct protocol is constructed. We now illustrate this process with a concrete example of how a simple cache coherence protocol might be constructed using this methodology).
Regarding claim 12,
Udupa teaches
wherein the synthesis algorithm comprises: detecting incompleteness in the input and output examples used in generating the logical specification (Fig.1.1,& Fig.4.1; Section 1.1 - The resulting implementation is then checked for correctness using some combination of verification and testing techniques. For example, testing techniques could be used to check for correct behavior with respect to different scenarios specified by the programmer, whereas verification techniques could check that the candidate protocol satisfies the high-level safety and liveness specifications set forth by the programmer. In the event that an error is found during this check for correctness, the verification or testing framework provides the programmer with a concrete execution of the candidate protocol that demonstrates the error);
generating a supplemental input example usable for generating the logical specification, requesting and receiving, from a user, a supplemental output example corresponding to the supplemental input example (Fig 4.3 -Section 1.1 - the verification or testing framework provides the programmer with a concrete execution of the candidate protocol that demonstrates the error. The programmer then uses this information to refine or correct the behavior of the candidate protocol in the context of the specific counterexample currently under consideration. This process often requires the programmer to reason globally about the protocol to avoid introducing new errors as in the corrected version of the protocol – Section 4.2 - transit allows the programmer to fuse a transition involving the receipt of a message with a transition involving transmitting an output message, i.e., an input or internal transition, followed immediately by an output transition - An attempt to verify the protocol instantiated with this update, results in a violation of the coherence invariant. A visual representation of a simplified version of the error trace is shown in Figure 4.3. Observe that the transition shown on the directory esm in Figure 4.3 is a concrete instance of the concolic snippet that we have described, with the cache esm C2 being Msg.Sender and the Owner variable of the directory esm Dir initially set to C1. Upon inspecting the error trace, the programmer recognized that in this particular case, the new value of the Sharers variable needed to include the previous value of the Owner variable as well. The programmer codifies this using the following concrete snippet Fig.4.1, the one counterexample. transit integrates the new (concrete) constraints with the rest of the constraints to provide a new interpretation I which satisfies all the constraints. The protocol is instantiated with the new interpretation, and the process is repeated until a correct protocol is found. The programmer is thus freed from reasoning about the global properties of the protocol when handling corner-case behavior, which were not handled in the initial version of the protocol);
and utilizing the supplemental input and output examples in generating the logical specification (Fig. 4.1, Section 4.1 - The programmer can then codify the fixes to any counterexamples obtained during this check using concrete input-output examples that correspond to a local fix, which eliminates at least the one counterexample transit integrates the new (concrete) constraints with the rest of the constraints to provide a new interpretation I which satisfies all the constraints. The protocol is instantiated with the new interpretation, and the process is repeated until a correct protocol is found – Section 6.3.3 - augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification).
Regarding claim 17,
Udupa further teaches
wherein the input and output examples include a first input example and a first output example, wherein the first input example includes network information, topology information, virtual machine (VM) configuration information, link cost information, or a weighted directed graph and the first output example includes network state information, shortest or best path information, or reachable VM pair information (Section 2.1 - . We allow the developer to specify a skeleton or sketch of the protocol that defines (i) the set of communicating processes that make up the protocol (ii) the state variables of each communicating process that is part of the protocol, (iii) the communication architecture of the protocol, which defines which processes can communicate, and along which direction, as well as describes the properties of communication links between processes- Section 1.1.1 - The working of the VI coherence protocol is perhaps best explained using the scenarios shown in Figure 1.3. The protocol consists of two classes of state machines: The cache controller state machines, whose behaviors are symmetric, denoted by C1, C2, . . . , Cn in Figure 1.3, and a singular directory state machine, denoted by D in Figure 1.3. Each cache machine has a state variable named cdata which contains the cached value of data at any point, and can be undefined if the cache does not have an up-do-date cached copy of the data).
Regarding claim 18,
Udupa further teaches
using the logical specification for verification, analysis, or prototyping purposes; or executing, using a compiler or interpreter, the logical specification and monitoring the execution of the logical specification for issues (Abstract - The programmer also specifies a set of high-level formal requirements that a correct protocol is expected to satisfy. These requirements can include safety requirements as well as liveness requirements in the form of Linear Temporal Logic formulas. We describe techniques to synthesize a correct protocol which is consistent with the common-case behavior specified by the programmer and also satisfies the high-level safety and liveness requirements set forth by the programmer – Section 1 - The programmer would also have to state the high-level correctness requirements for the protocol in a temporal logic of choice.1 The role of the synthesizer is to complete the incomplete protocol provided by the programmer, such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior – Section 1.1 - The resulting implementation is then checked for correctness using some combination of verification and testing techniques. For example, testing techniques could be used to check for correct behavior with respect to different scenarios specified by the programmer, whereas verification techniques could check that the candidate protocol satisfies the high-level safety and liveness specifications set forth by the programmer. In the event that an error is found during this check for correctness, the verification or testing framework provides the programmer with a concrete execution of the candidate protocol that demonstrates the error).
Regarding claim 20,
Udupa teaches a non-transitory computer readable medium having stored thereon executable instructions that when executed by a processor of a computer causes a computer to perform steps (Abstract), comprising:
receiving input and output examples associated with a network protocol; (Section 1 - Introduction - The role of the synthesizer is to complete the incomplete protocol provided by the programmer, such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior - These unknown functions could be used in the guards for transitions which describe the condition under which the transition in question can be executed and the update functions to state variables on transitions which describe how the state variables of the state machine evolve upon execution of the transition. The programmer could also provide some information on the missing behavior. This information might be in the form of input-output examples describing the behavior of the unknown functions, or could be information about exactly what behavior is left unspecified; To construct a protocol from the concolic snippets provided by the programmer, transit needs to synthesize expressions which are consistent with each of the snippets provided by the programmer. Let us, for the moment, assume that constraints implied by the programmer in the concolic snippets can be translated precisely into a constraint , of the form described in 57 Section 4.1. We will return to the question of how this translation is accomplished towards the end of this section. For the purpose of the synthesis algorithm, we treat the constraints obtained from both concrete and concolic snippets in the same way, i.e., as symbolic constraints over the expressions to be synthesized. For each unknown function);
generating, using the input and output examples and a synthesis algorithm, a logical specification defining the network protocol, wherein the logical specification includes a set of rules; and ( Section 1 – Introduction - In our formalization of the synthesis problem, processes communicate using input/output channels that carry typed messages. Each process is described by a state machine with a set of typed state variables. Transitions consist of guards — that test some condition over the state variables — and updates to state variables and fields of messages to be sent. Such guards and updates can involve unknown (typed) functions to be filled in by the synthesizer Section 8.1 - We model the unknown functions used in the guards and updates in the esm-sks as uninterpreted functions — rather than as Boolean variables as was the case in the algorithm described in Chapter 7 — and ask the SMT solver for an interpretation which satisfies the set of constraints maintained by the algorithm - See Algorithm 6.5, Section 6.3.3 - the algorithm eusolve, shown as Algorithm 6.5, shows how the Term Solve and Unify Terms algorithms are composed to form a complete SyGuS solver. The algorithm maintains a list of valuations P, which are built up from counterexamples returned by the algorithm Unify Terms. It repeatedly calls the algorithm Term Solve, followed by the algorithm Unify Terms, augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification - See Also Section 4..3
outputting the logical specification (Section 1 - The role of the synthesizer is to complete the incomplete protocol provided by the programmer such that the completed protocol (a) satisfies the high-level correctness requirements set forth by the programmer, and (b) is consistent with the information provided by the programmer about the unspecified behavior. This methodology for protocol specification can be viewed as a fruitful collaboration between the designer and the synthesis tool: the programmer has to describe the structure of the desired protocol, but some details that the programmer is unsure about, for instance, regarding corner cases and handling of unexpected messages, are filled in automatically by the tool – See Section 1.1 - This process often requires the programmer to reason globally about the protocol to avoid introducing new errors as in the corrected version of the protocol. This tedious process of discovering bugs and correcting the protocol is iterated until a correct protocol is constructed. We now illustrate this process with a concrete example of how a simple cache coherence protocol might be constructed using this methodology).
Claim Rejections - 35 USC § 103
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.
Claims 3,13 are rejected under 35 U.S.C. 103 as being unpatentable over Udupa in view of Arpit et al. “ A Novel Genetic Programming based Classifier Design using a New Constructive Crossover Operator with a Local Search Technique” Publication Date 2013 (Arpit hereinafter).
Regarding claim 3,
Udupa further teaches
wherein the synthesis algorithm utilizes a […] search algorithm that incrementally explores an unbounded search space in synthesizing the set of rules of the logical specification ( Abstract, Algorithm 6.2 & 6.3, Section 6.3.3 - the algorithm eusolve, shown as Algorithm 6.5, shows how the Term Solve and Unify Terms algorithms are composed to form a complete Sy Gu solver. The algorithm maintains a list of valuations P, which are built up from counterexamples returned by the algorithm Unify Terms. It repeatedly calls the algorithm Term Solve, followed by the algorithm Unify Terms augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification – Based on these observations, we now only need to prove that a sufficient set of terms and atomic predicates will eventually be enumerated by the Algorithm 6.3 and Algorithm 6.4 respectively. This follows from the observations of finiteness and progress made above, and the
fact that the sets defined by the grammars GT and GP are recursively enumerable Section 1.3 - Provide a common input language for specifying the constraints on, and the search space for candidate interpretations or bodies of unknown functions to be synthesized. This format, called SyGuS-IF, can then serve as a common input language for describing benchmarks to evaluate tools implementing different program synthesis technique Algorithm 6.2 expands the mapping L to include more terms. This is tantamount to expanding the set of terms that are allowed to be a part of a solution– Section 1.4 - We describe the SyGuS framework for specifying program synthesis problems in a general manner, which is intended to be an enabling technology for higher-level synthesis techniques to build upon. We also describe and evaluate algorithmic strategies based on systematic and intelligent enumerative search to solve instances of the SyGuS problem – Section 3.5.2 - the case of the symbolic algorithm, which uses a symbolic, breadth-first search strategy. In the later chapters of this dissertation, we explore heuristics for explicit state model checking algorithms, which lead to quicker convergence of the CEGIS loop to find an interpretation that satisfies the requirements described in Section 2.3. – Section 7.3.3 - We approximate this by finding a minimal path to a safety violation using breadth-first search. If the path contains a subset of the transitions in T, we remove all super-sets of that subset from the search space).
However, Udupa does not explicitly teach that the search is the best first search.
Arpit teaches
a best first search (Section 2, we propose to improve the crossover operation, by using the best first search technique to generate the offsprings. By using the best first search technique, we remove the randomness of crossover operation. Now we don’t have to search for crossover point to generate offsprings – Section 3.1 – In proposed crossover we applied a best first search to improve the overall crossover operation. In this crossover operation, we generate all the possible children from the parent. Then, we check the fitness of all the generated children. The two children with the highest fitness are chosen. Now we apply the elitism, fitness of the chosen children is compared with the parent. If the fitness of the chosen children is better than the parent, children are transferred to the next generation
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa to include the teachings of Arpit. The motivation for doing so is to allow system to use the first best search because it is highly efficient as it uses heuristics to guide the search towards the most promising nodes, reducing the search space.
Regarding claim 13,
Udupa further teaches
wherein the synthesis algorithm utilizes a […] search algorithm that incrementally explores an unbounded search space in synthesizing the set of rules of the logical specification ( Abstract, Algorithm 6.2 & 6.3, Section 6.3.3 - the algorithm eusolve, shown as Algorithm 6.5, shows how the Term Solve and Unify Terms algorithms are composed to form a complete Sy Gu solver. The algorithm maintains a list of valuations P, which are built up from counterexamples returned by the algorithm Unify Terms. It repeatedly calls the algorithm Term Solve, followed by the algorithm Unify Terms augmenting the list of valuations P in each iteration, until Unify Terms returns a solution that has been verified to be a correct solution to the SyGuS specification – Based on these observations, we now only need to prove that a sufficient set of terms and atomic predicates will eventually be enumerated by the Algorithm 6.3 and Algorithm 6.4 respectively. This follows from the observations of finiteness and progress made above, and the
fact that the sets defined by the grammars GT and GP are recursively enumerable Section 1.3 - Provide a common input language for specifying the constraints on, and the search space for candidate interpretations or bodies of unknown functions to be synthesized. This format, called SyGuS-IF, can then serve as a common input language for describing benchmarks to evaluate tools implementing different program synthesis technique Algorithm 6.2 expands the mapping L to include more terms. This is tantamount to expanding the set of terms that are allowed to be a part of a solution– Section 1.4 - We describe the SyGuS framework for specifying program synthesis problems in a general manner, which is intended to be an enabling technology for higher-level synthesis techniques to build upon. We also describe and evaluate algorithmic strategies based on systematic and intelligent enumerative search to solve instances of the SyGuS problem – Section 3.5.2 - the case of the symbolic algorithm, which uses a symbolic, breadth-first search strategy. In the later chapters of this dissertation, we explore heuristics for explicit state model checking algorithms, which lead to quicker convergence of the CEGIS loop to find an interpretation that satisfies the requirements described in Section 2.3. – Section 7.3.3 - We approximate this by finding a minimal path to a safety violation using breadth-first search. If the path contains a subset of the transitions in T, we remove all super-sets of that subset from the search space).
However, Udupa does not explicitly teach that the search is best first search.
Arpit teaches
a best first search (Section 2, we propose to improve the crossover operation, by using the best first technique to generate the offsprings. By using the best first search technique, we remove the randomness of crossover operation. Now we don’t have to search for crossover point to generate offsprings – Section 3.1 – In proposed crossover we applied a best first search to improve the overall crossover operation. In this crossover operation, we generate all the possible children from the parent. Then, we check the fitness of all the generated children. The two children with the highest fitness are chosen. Now we apply the elitism, fitness of the chosen children is compared with the parent. If the fitness of the chosen children is better than the parent, children are transferred to the next generation
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa to include the teachings of Arpit. The motivation for doing so is to allow system to use the first best search because it is highly efficient as it uses heuristics to guide the search towards the most promising nodes, reducing the search space.
Claims 4-5,14,16 rejected under 35 U.S.C. 103 as being unpatentable over Udupa in view of Arpit further in view of Landsborough et al. Publication No. US 2020/0012581 A1 ( Landsborough hereinafter)
Regarding claim 4,
Udupa in view of Arpit teaches best first search ( Arpit – Sections 2 & 3.1). However, Udupa in view of Arpit does not explicitly teach
the search algorithm comprises: performing an iterative loop until a stop condition is reached, the iterative loop including: mutating, using at least one mutation strategy, a first candidate specification to generate a plurality of offspring candidates, wherein each of the plurality of offspring candidates are scored; and selecting, from the plurality of offspring candidates and using scores of the plurality of offspring candidates, a second candidate specification to mutate
Landsborough teaches
search algorithm comprises: performing an iterative loop until a stop condition is reached, the iterative loop including (¶0020 - an improved program transform routine incorporating Method 10 could iteratively (and potentially randomly) apply multiple, independent patches to target binaries in order to safely affect their size, features, performance, and security-related properties – ¶0023 -The overall approach of Method 10 consists of the following steps: (1) mutating the target program binary in place, producing a plurality of variants, Step 10a; (2) testing each variant for validity using a test suite, Step; (3) discarding variants which fail, Step 1 Od; ( 4) comparing each variant that passes to the original program (the target program binary), Step l0e; (5) extracting candidate transforms which meet the scope criteria – ¶0026 -This approach is very straightforward and allows for fast program mutation. FIG. 3 shows the percentage of executable code in bytes modified in the resulting binaries (variants) generated by running the genetic algorithm on the core util binaries for 500,000 evaluations. There was approximately a 50 percent change in the bytes in the executable sections of each of the binaries with a few notable outliers);
mutating, using at least one mutation strategy, a first candidate specification to generate a plurality of offspring candidates, wherein each of the plurality of offspring candidates are scored ( ¶0024 - A genetic algorithm comprises a population of candidates (for example, the target binaries at Step 10a) which are mutated and combined to create new individuals within the population. This population is maintained through selection. While multiple methods of selection are available, Method 10 uses tournament selection. In tournament selection, multiple candidates are compared, and the one with the best fitness is selected to evolve, while the one with a worse fitness is rejected from the population. The fitness of each candidate is determined using a fitness function. In the case of evolving software, the fitness function includes validation using some number of test cases. Individuals that fail test cases will get a bad fitness score. Individuals that pass the test cases are given a fitness which is measured by the desired
optimization or specialization criteria) ; and
selecting, from the plurality of offspring candidates and using scores of the plurality of offspring candidates, a second candidate specification to mutate( ¶0024 - Method 10 uses tournament selection. In tournament selection, multiple candidates are compared, and the one with the best fitness is selected to evolve, while the one with a worse fitness is rejected from the population. The fitness of each candidate is determined using a fitness function. The fitness of each candidate is determined using a fitness function. In the case of evolving software, the fitness function includes validation using some number of test cases. Individuals that fail test cases will get a bad fitness score. Individuals that pass the test cases are given a fitness which is measured by the desired optimization or specialization criteria (such as program size, program performance, program energy usage, or program diversity). Mutations are probabilistic changes to an individual. The mutation operations used for evolving software can include inserting code, swapping two code snippets, and deleting code) .
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa in view Arpit to include the teachings of Landsborough. The motivation for doing so is to allow system to mutate and evolve software, extracting useful software transforms from the ecosystem of program variants resulting from evolution using traditional genetic algorithm approaches (Landsborough – ¶0016).
Regarding claim 5,
Udupa does not explicitly teach
wherein the second candidate specification to mutate is selected from offspring candidates of the plurality of offspring candidates that have higher scores or is selected from the plurality of offspring candidates when none of the plurality of offspring candidates has a higher score
However, Landsborough teaches
wherein the second candidate specification to mutate is selected from offspring candidates of the plurality of offspring candidates that have higher scores or is selected from the plurality of offspring candidates when none of the plurality of offspring candidates has a higher score (¶ 0024 - Method 10 uses tournament selection. In tournament selection, multiple candidates are compared, and the one with the best fitness is selected to evolve, while the one with a worse fitness is rejected from the population. The fitness of each candidate is determined using a fitness function. The fitness of each candidate is determined using a fitness function. In the case of evolving software, the fitness function includes validation using some number of test cases. Individuals that fail test cases will get a bad fitness score. Individuals that pass the test cases are given a fitness which is measured by the desired optimization or specialization criteria (such as program size, program performance, program energy usage, or program diversity). Mutations are probabilistic changes to an individual. The mutation operations used for evolving software can include inserting code, swapping two code snippets, and deleting code).
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa to include the teachings of Landsborough. The motivation for doing so is to allow system to mutate and evolve software, extracting useful software transforms from the ecosystem of program variants resulting from evolution using traditional genetic algorithm approaches (Landsborough – ¶ 0016).
Regarding claim 14,
Udupa in view of Arpit teaches best first search ( Arpit – Sections 2 & 3.1). However, Udupa in view of Arpit does not explicitly teach
the search algorithm comprises: performing an iterative loop until a stop condition is reached, the iterative loop including: mutating, using at least one mutation strategy, a first candidate specification to generate a plurality of offspring candidates, wherein each of the plurality of offspring candidates are scored; and selecting, from the plurality of offspring candidates and using scores of the plurality of offspring candidates, a second candidate specification to mutate
Landsborough teaches
search algorithm comprises: performing an iterative loop until a stop condition is reached, the iterative loop including (¶0020 - an improved program transform routine incorporating Method 10 could iteratively (and potentially randomly) apply multiple, independent patches to target binaries in order to safely affect their size, features, performance, and security-related properties – ¶0023 -The overall approach of Method 10 consists of the following steps: (1) mutating the target program binary in place, producing a plurality of variants, Step 10a; (2) testing each variant for validity using a test suite, Step; (3) discarding variants which fail, Step 1 Od; ( 4) comparing each variant that passes to the original program (the target program binary), Step l0e; (5) extracting candidate transforms which meet the scope criteria – ¶ 0026 -This approach is very straightforward and allows for fast program mutation. FIG. 3 shows the percentage of executable code in bytes modified in the resulting binaries (variants) generated by running the genetic algorithm on the core util binaries for 500,000 evaluations. There was approximately a 50 percent change in the bytes in the executable sections of each of the binaries with a few notable outliers.);
mutating, using at least one mutation strategy, a first candidate specification to generate a plurality of offspring candidates, wherein each of the plurality of offspring candidates are scored ( ¶0024 - A genetic algorithm comprises a population of candidates (for example, the target binaries at Step 10a) which are mutated and combined to create new individuals within the population. This population is maintained through selection. While multiple methods of selection are available, Method 10 uses tournament selection. In tournament selection, multiple candidates are compared, and the one with the best fitness is selected to evolve, while the one with a worse fitness is rejected from the population. The fitness of each candidate is determined using a fitness function. In the case of evolving software, the fitness function includes validation using some number of test cases. Individuals that fail test cases will get a bad fitness score. Individuals that pass the test cases are given a fitness which is measured by the desired
optimization or specialization criteria) ; and
selecting, from the plurality of offspring candidates and using scores of the plurality of offspring candidates, a second candidate specification to mutate( ¶0024 - Method 10 uses tournament selection. In tournament selection, multiple candidates are compared, and the one with the best fitness is selected to evolve, while the one with a worse fitness is rejected from the population. The fitness of each candidate is determined using a fitness function. The fitness of each candidate is determined using a fitness function. In the case of evolving software, the fitness function includes validation using some number of test cases. Individuals that fail test cases will get a bad fitness score. Individuals that pass the test cases are given a fitness which is measured by the desired optimization or specialization criteria (such as program size, program performance, program energy usage, or program diversity). Mutations are probabilistic changes to an individual. The mutation operations used for evolving software can include inserting code, swapping two code snippets, and deleting code) .
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa in view Arpit to include the teachings of Landsborough. The motivation for doing so is to allow system to mutate and evolve software, extracting useful software transforms from the ecosystem of program variants resulting from evolution using traditional genetic algorithm approaches (Landsborough – ¶0016).
Regarding claim 16,
Udupa does not explicitly teach
wherein the second candidate specification to mutate is selected from offspring candidates of the plurality of offspring candidates that have higher scores or is selected from the plurality of offspring candidates when none of the plurality of offspring candidates has a higher score
However, Landsborough teaches
wherein the second candidate specification to mutate is selected from offspring candidates of the plurality of offspring candidates that have higher scores or is selected from the plurality of offspring candidates when none of the plurality of offspring candidates has a higher score (¶0024 - Method 10 uses tournament selection. In tournament selection, multiple candidates are compared, and the one with the best fitness is selected to evolve, while the one with a worse fitness is rejected from the population. The fitness of each candidate is determined using a fitness function. The fitness of each candidate is determined using a fitness function. In the case of evolving software, the fitness function includes validation using some number of test cases. Individuals that fail test cases will get a bad fitness score. Individuals that pass the test cases are given a fitness which is measured by the desired optimization or specialization criteria (such as program size, program performance, program energy usage, or program diversity). Mutations are probabilistic changes to an individual. The mutation operations used for evolving software can include inserting code, swapping two code snippets, and deleting code) ..
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa to include the teachings of Landsborough. The motivation for doing so is to allow system to mutate and evolve software, extracting useful software transforms from the ecosystem of program variants resulting from evolution using traditional genetic algorithm approaches (Landsborough – ¶ 0016).
Claims 6,15 are rejected under 35 U.S.C. 103 as being unpatentable over Udupa in view of Arpit further in view of Landsborough further in view of Chen et al. “ Towards Example-Guided Network Synthesis” Publication date 2018 ( Chen hereinafter)
Regarding claim 6,
Udupa in view of Landsborough does not explicitly teach
wherein the at least one mutation strategy includes adding a new rule, extending an existing rule, or applying an aggregation operator.
However, Chen teaches
wherein the at least one mutation strategy includes adding a new rule, extending an existing rule, or applying an aggregation operator ( Section 4.1 &4,2 - The outer loop adds a new rule to the program. The inner loop finds the next rule to add, by iterating over syntactically correct rules and evaluating it against the input-output examples. A rule r is added if it produces some positive outputs, and no negative output – Section 4.3 - Algorithm 1 is complete. By the analysis in section 4.2, all syntactically valid rules are enumerated, and verified for
correctness. If there exists a correct solution, that is, a set of rules that produces the desired outputs, algorithm 1 always returns one. If there does not exist a correct solution, algorithm 1 always terminates with a failure. Therefore, algorithm 1 is complete).
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa in view of Landsborough to include the teachings of Chen. The motivation for doing so is to allow system to provide efficient search algorithm that exploits syntactic constraints in declarative networking to prune the search space, and semantics as heuristics to guide the search direction (Chen– Abstract).
Regarding claim 15,
Udupa in view of Landsborough does not explicitly teach
wherein the at least one mutation strategy includes adding a new rule, extending an existing rule, or applying an aggregation operator.
However, Chen teaches
wherein the at least one mutation strategy includes adding a new rule, extending an existing rule, or applying an aggregation operator ( Section 4.1 &4,2 - The outer loop adds a new rule to the program. The inner loop finds the next rule to add, by iterating over syntactically correct rules and evaluating it against the input-output examples. A rule r is added if it produces some positive outputs, and no negative output – Section 4.3 - Algorithm 1 is complete. By the analysis in section 4.2, all syntactically valid rules are enumerated, and verified for
correctness. If there exists a correct solution, that is, a set of rules that produces the desired outputs, algorithm 1 always returns one. If there does not exist a correct solution, algorithm 1 always terminates with a failure. Therefore, algorithm 1 is complete).
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa in view of Landsborough to include the teachings of Chen. The motivation for doing so is to allow system to provide efficient search algorithm that exploits syntactic constraints in declarative networking to prune the search space, and semantics as heuristics to guide the search direction (Chen– Abstract).
Claims 10,19 are rejected under 35 U.S.C. 103 as being unpatentable over Udupa in view of Chen
Regarding claim 10,
Udupa does not explicitly teach
wherein the logical specification is expressed using a declarative logic programming language, Datalog, or an extended Datalog like language.
However, Chen teaches
wherein the logical specification is expressed using a declarative logic programming language, Datalog, or an extended Datalog like language (Section 1 - As the first step towards realizing our eventual vision for Facon, we perform a feasibility study of Facon, through a case study of Network Datalog (NDLog) [11], a representative declarative networking language. Section 2.2 - In this paper, we focus on synthesizing NDLog programs which is a dialect of the Datalog language, commonly used in the database community for querying graphs. The language is based on logic, and we provide some preliminaries on logic programming – See Section 6 – synthesizes general Datalog programs using input-output examples. It translates syntax and examples into constraints, and uses SMT solver to find the target program. )
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa to include the teachings of Chen. The motivation for doing so is to allow system to provide efficient search algorithm that exploits syntactic constraints in declarative networking to prune the search space, and semantics as heuristics to guide the search direction (Chen– Abstract).
Regarding claim 19,
Udupa does not explicitly teach
wherein the logical specification is expressed using a declarative logic programming language, Datalog, or an extended Datalog like language.
However, Chen teaches
wherein the logical specification is expressed using a declarative logic programming language, Datalog, or an extended Datalog like language (Section 1 - As the first step towards realizing our eventual vision for Facon, we perform a feasibility study of Facon, through a case study of Network Datalog (NDLog) [11], a representative declarative networking language. Section 2.2 - In this paper, we focus on synthesizing NDLog programs which is a dialect of the Datalog language, commonly used in the database community for querying graphs. The language is based on logic, and we provide some preliminaries on logic programming – See Section 6 – synthesizes general Datalog programs using input-output examples. It translates syntax and examples into constraints, and uses SMT solver to find the target program. )
It would have been obvious to a person of ordinary skill in the art before the effective filing date of the claimed invention to modify the teachings of Udupa to include the teachings of Chen. The motivation for doing so is to allow system to provide efficient search algorithm that exploits syntactic constraints in declarative networking to prune the search space, and semantics as heuristics to guide the search direction (Chen– Abstract).
Conclusion
Any inquiry concerning this communication or earlier communications from the examiner should be directed to YOUNES NAJI whose telephone number is (571)272-2659. The examiner can normally be reached Monday - Friday 8:30 AM -5:30 PM.
Examiner interviews are available via telephone, in-person, and video conferencing using a USPTO supplied web-based collaboration tool. To schedule an interview, applicant is encouraged to use the USPTO Automated Interview Request (AIR) at http://www.uspto.gov/interviewpractice.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Oscar A Louie can be reached on (571) 270-1684. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of published or unpublished applications may be obtained from Patent Center. Unpublished application information in Patent Center is available to registered users. To file and manage patent submissions in Patent Center, visit: https://patentcenter.uspto.gov. Visit https://www.uspto.gov/patents/apply/patent-center for more information about Patent Center and https://www.uspto.gov/patents/docx for information about filing in DOCX format. For additional questions, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/YOUNES NAJI/Primary Examiner, Art Unit 2445