DETAILED ACTION
This office action has been issued in response to communications received on 3/25/2024 and 2/10/2026. Claims 18-20 were cancelled in response to a restriction requirement and new claims 21-23 were added. Claims 1-17 and 21-23 are presented for examination. The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
Drawings
The drawings filed on 3/25/2024 are acknowledged.
Priority
Provisional priority to 2/26/2024 is recognized.
RESTRICTION
Applicant’s selection of group 1 (comprising claims 1-17) without traverse is acknowledged. Accordingly, the restriction is MADE FINAL.
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 of this title, 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.
The factual inquiries set forth in Graham v. John Deere Co., 383 U.S. 1, 148 USPQ 459 (1966), that are applied for establishing a background for determining obviousness under 35 U.S.C. 103 are summarized as follows:
1. Determining the scope and contents of the prior art.
2. Ascertaining the differences between the prior art and the claims at issue.
3. Resolving the level of ordinary skill in the pertinent art.
4. Considering objective evidence present in the application indicating obviousness or non-obviousness.
This application currently names joint inventors. In considering patentability of the claims the examiner presumes that the subject matter of the various claims was commonly owned as of the effective filing date of the claimed invention(s) absent any evidence to the contrary. Applicant is advised of the obligation under 37 CFR 1.56 to point out the inventor and effective filing dates of each claim that was not commonly owned as of the effective filing date of the later invention in order for the examiner to consider the applicability of 35 U.S.C. 102(b)(2)(C) for any potential 35 U.S.C. 102(a)(2) prior art against the later invention.
In the event the determination of the status of the application as subject to AIA 35 U.S.C. 102 and 103 (or as subject to pre-AIA 35 U.S.C. 102 and 103) is incorrect, any correction of the statutory basis for the rejection will not be considered a new ground of rejection if the prior art relied upon, and the rationale supporting the rejection, would be the same under either status.
Claims 1, 5-9, 13-16, and 21-23 are rejected under 35 U.S.C. 103 as being unpatentable over Goel (US 2025/0106256) in view of Yakir Vizel et al., Fast Interpolating BMC, Lecture Notes in Computer Science (July 2015) (hereafter “Vizel”).
Regarding claim 1, Goel discloses the limitations of claim 1 substantially as follows:
A computer-implemented method for validating role-based access control (RBAC) policies comprising:
identifying an RBAC policy and a validation property to validate an intended specification of the RBAC policy (paras. [0018]: identifying role-based access control policies that define and express security requirements for resources and properties of the policies to be validated);
generating a symbolic expression of the RBAC policy that violates the validation property using a symbolic abstraction model (paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the symbolic expression into a satisfiability function representation to be solved by a satisfiability solver model (paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on receiving a counterexample from the satisfiability solver model, determining that the RBAC policy is invalid for the validation property (paras. [0072]-[0074]: receiving from the model/SMT solver a counterexample of the access control policy and determining that the property does not hold for all states (i.e. validation property and corresponding policy are invalid)).
Goel does not explicitly disclose the remaining limitations of claim 1 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model
However, in the same field of endeavor Vizel discloses the limitations of claim 1 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model (abstract, Introduction, Bounded Model Checking, pp. 5-6: after finding a counterexample that represents a property that fails to be proved as safe in the BMC and is unsafe, symbolically represent them as expressions in a transition system (i.e. generate symbolic counterexample expressions) and then use a SAT solver to check for their existence))
Goel is combinable with Vizel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Vizel’s method of generating symbolic counterexample expressions and verifying them using a SAT solver with the system of Goel in order in improve the accuracy of determining counterexamples by enabling testing their symbolic expressions in a SAT model to verify the validity of the error represented by the counterexample and refine the search process for additional counterexamples.
Regarding claim 5, Goel and Vizel disclose the limitations of claim 1.
Goel discloses the limitations of claim 5 as follows:
The computer-implemented method of claim 1, wherein the RBAC policy is part of a set of RBAC policies implemented by a cloud computing system to authorize access to resources of the cloud computing system (paras. [0017]-[0018], [0023]:role-based access control policies are implemented by a cloud network environment comprising cloud-based applications and authorizing access to resources of the environment).
Regarding claim 6, Goel and Vizel disclose the limitations of claim 1.
Goel discloses the limitations of claim 6 as follows:
The computer-implemented method of claim 1, wherein the symbolic abstraction model generates the symbolic counterexample expression into a common intermediate language that encodes semantics of multiple source languages (paras. [0016], [0020], [0054], [0058]: the policies are compiled into a unified policy language broad enough to include diverse policy features, yet specific enough for automated analysis).
Regarding claim 7, Goel and Vizel disclose the limitations of claim 1.
Goel discloses the limitations of claim 7 as follows:
The computer-implemented method of claim 1, wherein the counterexample includes a user requirement input that violates the RBAC policy (paras. [0017], [0072]-[0074]: counterexample indicates that a property relating an access control policy requiring a user to meet the elements defined in the policy to be authorized fails when input into the model checker (i.e. property violates the RBAC policy by not being true for all states)).
Regarding claim 8, Goel and Vizel disclose the limitations of claims 1 and 7.
Goel discloses the limitations of claim 8 as follows:
The computer-implemented method of claim 7, wherein the user requirement input includes a principal value, an action value, and a scope value (paras. [0047]: access control policies specify the principal, and action and the resources impacted/scope).
Regarding claim 9, Goel and Vizel disclose the limitations of claims 1 and 7-8.
Goel discloses the limitations of claim 9 as follows:
The computer-implemented method of claim 8, wherein the user requirement input is provided to a cloud computing system to request access to a resource of the cloud computing system (paras. [0016], [0027], [0033], [0062], [0063], [0131]: requests by a user to access resources of cloud services/provider are subject to the access control policies).
Regarding claim 13, Goel and Vizel disclose the limitations of claim 1.
Goel and Vizel discloses the limitations of claim 13 as follows:
The computer-implemented method of claim 1, further comprising:
generating a second symbolic counterexample expression (Vizel, abstract, Introduction, Bounded Model Checking, pp. 5-6: after finding a counterexample that represents a property that fails to be proved as safe in the BMC and is unsafe, symbolically represent them as expressions in a transition system (i.e. generate symbolic counterexample expressions) of the RBAC policy violating a second validation property using the symbolic abstraction model (Goel, paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the second symbolic counterexample expression (Vizel, abstract, Introduction, Bounded Model Checking, pp. 5-6: after finding a counterexample that represents a property that fails to be proved as safe in the BMC and is unsafe, symbolically represent them as expressions in a transition system (i.e. generate symbolic counterexample expressions) into a second satisfiability function representation to be solved by the satisfiability solver model (Goel, paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on failing to receive any counterexample from the satisfiability solver model, determining that the RBAC policy is valid for the validation property (paras. [0072]-[0074]: based on not receiving a counterexample from the model/SMT solver, determining that the property holds true for all states (i.e. validation property and corresponding policy are valid)).
The same motivation to combine utilized in claim 1 is equally applicable in the instant claim.
Regarding claim 14, Goel discloses the limitations substantially as follows:
A system for validating role-based access control (RBAC) policies comprising:
a processing system; and
a computer memory comprising instructions that, when executed by the processing system, cause the system to perform operations of:
identifying an RBAC policy and a validation property to validate an intended specification of the RBAC policy (paras. [0018]: identifying role-based access control policies that define and express security requirements for resources and properties of the policies to be validated);
generating a symbolic expression of the RBAC policy that violates the validation property using a symbolic abstraction model (paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the symbolic expression into a satisfiability function representation to be solved by a satisfiability solver model (paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on receiving a counterexample from the satisfiability solver model, determining that the RBAC policy is invalid for the validation property (paras. [0072]-[0074]: receiving from the model/SMT solver a counterexample of the access control policy and determining that the property does not hold for all states (i.e. validation property and corresponding policy are invalid)).
Goel does not explicitly disclose the remaining limitations of claim 14 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model
However, in the same field of endeavor Vizel discloses the limitations of claim 14 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model (abstract, Introduction, Bounded Model Checking, pp. 5-6: after finding a counterexample that represents a property that fails to be proved as safe in the BMC and is unsafe, symbolically represent them as expressions in a transition system (i.e. generate symbolic counterexample expressions) and then use a SAT solver to check for their existence))
Goel is combinable with Vizel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Vizel’s method of generating symbolic counterexample expressions and verifying them using a SAT solver with the system of Goel in order in improve the accuracy of determining counterexamples by enabling testing their symbolic expressions in a SAT model to verify the validity of the error represented by the counterexample and refine the search process for additional counterexamples.
Regarding claim 15, Goel and Vizel disclose the limitations of claim 14.
Goel discloses the limitations of claim 15 as follows:
The system of claim 14, wherein the satisfiability solver model is a satisfiability modulo theories (SMT) solver (paras. [0072]-[0074] satisfiability solver model SMT solver).
Regarding claim 16, Goel and Vizel disclose the limitations of claim 14.
Goel discloses the limitations of claim 16 as follows:
The system of claim 14, wherein the satisfiability solver model utilizes Boolean, arithmetic, bit-vectors, arrays, or uninterpreted functions to solve the satisfiability function representation (paras. [0067], [0070], [0072]-[0074]: the quotiented target access control policies are converted into a logic-based representation which the satisfiability solver analyzes (using Boolean for logic) defining behaviors as theorems (i.e. uninterpreted functions)).
Regarding claim 21 Goel discloses the limitations substantially as follows:
A non-transitory computer-readable storage medium for validating role-based access control (RBAC) policies comprising, and comprising instructions that, when executed by a processor, cause a computing device to carry out operations comprising:
identifying an RBAC policy and a validation property to validate an intended specification of the RBAC policy (paras. [0018]: identifying role-based access control policies that define and express security requirements for resources and properties of the policies to be validated);
generating a symbolic expression of the RBAC policy that violates the validation property using a symbolic abstraction model (paras. [0056]-[0057], [0070], [0072]: converting the source access control policy into a stream of tokens by recognizing keywords, operators, identifiers and other source access control policy-specific elements and generating a parse tree or abstract syntax tree representing the syntactic structure of the access control policy (i.e. generating symbolic expressions of the RBAC policy), further abstracting the policy by quotienting);
converting the symbolic expression into a satisfiability function representation to be solved by a satisfiability solver model (paras. [0065]-[0067], [0070], [0072]-[0073]: further abstracting the policy represented by the syntactic structure of the abstract syntax tree by quotienting (i.e. converting the symbolic expression) the target access control policies and generating a logic-based representation to be input/solved by a Satisfiability Modulo Theories (SMT) solver); and
based on receiving a counterexample from the satisfiability solver model, determining that the RBAC policy is invalid for the validation property (paras. [0072]-[0074]: receiving from the model/SMT solver a counterexample of the access control policy and determining that the property does not hold for all states (i.e. validation property and corresponding policy are invalid)).
Goel does not explicitly disclose the remaining limitations of claim 21 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model
However, in the same field of endeavor Vizel discloses the limitations of claim 21 as follows:
symbolic counterexample expression that violates the validation property using a symbolic abstraction model (abstract, Introduction, Bounded Model Checking, pp. 5-6: after finding a counterexample that represents a property that fails to be proved as safe in the BMC and is unsafe, symbolically represent them as expressions in a transition system (i.e. generate symbolic counterexample expressions) and then use a SAT solver to check for their existence))
Goel is combinable with Vizel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Vizel’s method of generating symbolic counterexample expressions and verifying them using a SAT solver with the system of Goel in order in improve the accuracy of determining counterexamples by enabling testing their symbolic expressions in a SAT model to verify the validity of the error represented by the counterexample and refine the search process for additional counterexamples.
Regarding claim 22, Goel and Vizel disclose the limitations of claim 21.
Goel discloses the limitations of claim 22 as follows:
The non-transitory computer-readable storage medium claim 21, wherein:
the counterexample includes a user requirement input that violates the RBAC policy (paras. [0017], [0072]-[0074]: counterexample indicates that a property relating an access control policy requiring a user to meet the elements defined in the policy to be authorized fails when input into the model checker (i.e. property violates the RBAC policy by not being true for all states));
the user requirement input includes a principal value, an action value, and a scope value (paras. [0047]: access control policies specify the principal, and action and the resources impacted/scope); and
the user requirement input is provided to a cloud computing system to request access to a resource of the cloud computing system (paras. [0016], [0027], [0033], [0062], [0063], [0131]: requests by a user to access resources of cloud services/provider are subject to the access control policies).
Regarding claim 23, Goel and Vizel disclose the limitations of claim 21.
Goel discloses the limitations of claim 23 as follows:
The non-transitory computer-readable storage medium claim 21, wherein the symbolic abstraction model generates the symbolic counterexample expression into a common intermediate language that encodes semantics of multiple source languages (paras. [0016], [0020], [0054], [0058]: the policies are compiled into a unified policy language broad enough to include diverse policy features, yet specific enough for automated analysis).
Claims 2-4, 10-12 and 17 are rejected under 35 U.S.C. 103 as being unpatentable over Goel (US 2025/0106256) in view of Yakir Vizel et al., Fast Interpolating BMC, Lecture Notes in Computer Science (July 2015) (hereafter “Vizel”), as applied to claims 1 and 14, further in view of Bolignano (US 11483317).
Regarding claim 2, Goel and Vizel disclose the limitations of claim 1.
Goel discloses the limitations of claim 2 as follows:
The computer-implemented method of claim 1, wherein the RBAC policy defines an effect, a principal, an action, (paras. [0018], [0047]-[0048]: components of an access control policy define include principals, actions, the outcome/effect -whether the action is allowed or denied).
Neither Goel or Vizel disclose a not-action, however in the same field of endeavor Bolignano discloses a non-action (col. 25, ll. 45-60: NotAction element would apply to all actions except those listed).
Bolignano is combinable with Vizel and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of using NonActions to define statements and matching elements with the system of Vizel and Goel in order to increase the flexibility of the system by enabling the system to specify policies or permissions that should be excluded.
Regarding claim 3, Goel, Vizel and Bolignano disclose the limitations of claims 1 and 2.
Goel discloses the limitations of claim 3 as follows:
The computer-implemented method of claim 2, wherein the RBAC policy defines a scope and a condition (paras. [0018], [0047]-[0048]: components of an access control policy define the resources the policy applies to (i.e. scope) and a condition).
Regarding claim 4, Goel, Vizel and Bolignano disclose the limitations of claims 1-2.
Goel discloses the limitations of claim 4 as follows:
The computer-implemented method of claim 2, wherein the effect is to deny or allow a request based on corresponding definitions being satisfied (paras. [0016], [0047]: policies are granted or denied based upon whether they are satisfied).
Regarding claim 10, Goel and Vizel disclose the limitations of claim 1.
Neither Goel or Vizel disclose the limitations of claim 10, however in the same field of endeavor, Bolignano discloses the limitations of claim 10 as follows:
The computer-implemented method of claim 1, further comprising modifying the RBAC policy to disallow the counterexample based on determining that the RBAC policy is vulnerable to allowing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: modifying the security policy/requirement specifying a user’s access rights based upon their role (i.e. RBAC policy) to prevent an event detected as leading to a counterexample from reoccurring based upon receiving a notification that the security requirement was violated (i.e. that the policy is vulnerable to being violated).
Bolignano does not explicitly disclose that the policy is modified in order to prevent the counterexample from being triggered but it would have been obvious to one of ordinary skill in the art that Bolignano discloses such functionality because Bolignano discloses the security policy may be deleted or changed after receiving a notification that a current security requirement was violated by a counter-example, therefore one of ordinary skill in the art would have found it obvious that the proposed change could be use the information from the notification to revise the security policy to prevent the violation from reoccurring.
Bolignano is combinable with Vizel and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of changing or deleting a security policy to prevent reoccurrence of a violation of the security policy with the system of Vizel and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Regarding claim 11, Goel and Vizel disclose the limitations of claim 1.
Neither Goel or Vizel disclose the limitations of claim 11, however in the same field of endeavor, Bolignano discloses the limitations of claim 11 as follows:
The computer-implemented method of claim 1, further comprising removing the RBAC policy based on determining that the RBAC policy is vulnerable to allowing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: deleting the security policy/requirement specifying a user’s access rights based upon their role (i.e. RBAC policy) to prevent an event detected as leading to a counterexample from reoccurring based upon receiving a notification that the security requirement was violated (i.e. that the policy is vulnerable to being violated).
Bolignano does not explicitly disclose that the policy is deleted in order to prevent the counterexample from being triggered but it would have been obvious to one of ordinary skill in the art that Bolignano discloses such functionality because Bolignano discloses the security policy may be deleted or changed after receiving a notification that a current security requirement was violated by a counter-example, therefore one of ordinary skill in the art would have found it obvious that the proposed deletion could be use the information from the notification to revise the security policy to prevent the violation from reoccurring.
Bolignano is combinable with Vizel and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of changing or deleting a security policy to prevent reoccurrence of a violation of the security policy with the system of Vizel and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Regarding claim 12, Goel and Vizel disclose the limitations of claim 1.
Neither Goel or Vizel disclose the limitations of claim 12, however in the same field of endeavor, Bolignano discloses the limitations of claim 12 as follows:
The computer-implemented method of claim 1, further comprising flagging the RBAC policy for review based on determining that the RBAC policy is vulnerable to performing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: sending the administrator a notification about a security policy/requirement specifying a user’s access rights based upon their role (i.e. RBAC policy) which has been violated (i.e. flatting the RBAC policy for review) based on determining that a counter-example violation of the policy has occurred (i.e. it is vulnerable to adverse actions)).
Bolignano is combinable with Vizel and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of changing or deleting a security policy to prevent reoccurrence of a violation of the security policy with the system of Vizel and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Regarding claim 17, Goel and Vizel disclose the limitations of claim 14.
Neither Goel or Vizel disclose the limitations of claim 17, however in the same field of endeavor, Bolignano discloses the limitations of claim 17 as follows:
The system of claim 14, wherein determining that the RBAC policy is invalid for the validation property includes determining that the RBAC policy is vulnerable to allowing adverse actions (col. 9, ll. 40-48, col. 10, ll. 5-10, 25-30, 42-46 & 58-65: receiving a notification with a counter-example indicating that the security policy was violated (i.e. determining that the policy needs to be amended because it is vulnerable to being violated) and proposing to change or delete a security policy).
Bolignano does not explicitly disclose that the policy is determined to be invalid (i.e. in need of being changed or deleted) based upon the notification, but it would have been obvious to one of ordinary skill in the art that Bolignano discloses such functionality because Bolignano discloses receiving notifications when a security policy has been violated, therefore it would be obvious to one of ordinary skill in the art that an administrator receiving multiple notifications about a particular security policy always being violated would determine that security policy needs to be either changed or replaced (i.e. because the policy is invalid).
Bolignano is combinable with Vizel and Goel because all are from the same field of generating symbolic expressions and testing the expressions for validity. It would have been obvious to one of ordinary skill in the art before the effective filing date of the claimed invention to integrate Bolignano’s method of providing notifications of violations of security policies and enabling changing or deleting a security policy with the system of Vizel and Goel in order to increase the security of the system by enabling the system to identify weaknesses in security policies by tracking violations of the security policies and to fix the weaknesses in the security policies by updating or removing flawed security policies.
Prior art not relied upon but applied/considered includes:
1) Ganai (US 2010/0305919) disclosing A method for symbolic model checking of sequential systems includes alternating between state-based and state-less symbolic model checking methods by combining a Presburger-based Symbolic technique (state-based), and SMT-based Bounded Model Checking (stateless) in a tightly integrated tool called a HMC (Hybrid Model Checker). A state-based approach such as MIX model checking may be employed to compute a reachable state set in a breadth-first search (BFS) up to some depth. With each partition S.sub.p as the state constraint at depth d, we use satisfiability modulo theories (SMT)-based bounded model checking (BMC) from the depth d to check if error blocks can be reached or show that termination is reached. Using the set S.sub.p as a state constraint depth d, starting BMC depth d, we invoke SMT-based BMC to check for counter-examples (CEX) for the error blocks E in block 29. If we find CEX, we update the set E. In block 30, if all error blocks are reached i.e. |E|=0, we stop in block 38. If for the input state constraint S.sub.p, we reach the completeness threshold, i.e., we explored all the paths, we return "termination reached" status. Otherwise, we return when a predetermined resource is exhausted. we consider symbolic formulas with Boolean expressions bool-expr and integer term expressions int-expr in Presburger arithmetic, a decidable subset of first-order theory. (paras. [0008], [0020], [0021], [0038], [0053]).
Conclusion
For the above reasons, claims 1-17 and 21-23 are rejected.
Any inquiry concerning this communication or earlier communications from the examiner should be directed to SHARON S LYNCH whose telephone number is (571)272-4583. The examiner can normally be reached on 10AM-6PM.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Taghi T Arani can be reached on 571-272-3787. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of an application may be obtained from the Patent Application Information Retrieval (PAIR) system. Status information for published applications may be obtained from either Private PAIR or Public PAIR. Status information for unpublished applications is available through Private PAIR only. For more information about the PAIR system, see http://pair-direct.uspto.gov. Should you have questions on access to the Private PAIR system, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative or access to the automated information system, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/SHARON S LYNCH/Primary Examiner, Art Unit 2438