Ambient calculus-based modal logic model checking
First Claim
1. A computer-implemented method that facilitates ambient calculus-based modal logic model checking, comprising:
- performing an analysis on an ambient calculus-based representation of a process with a formula that is represented via ambient calculus; and
outputting a result of the analysis that is utilized to facilitate determining whether the process satisfies the formula.
2 Assignments
0 Petitions
Accused Products
Abstract
Ambient calculus-based modal logic model checking is disclosed. In one embodiment, a method receives a process for analysis against a formula, and outputs whether it satisfies the formula. In one embodiment, process analysis is conducted in a recursive manner. The process is normalized to determine whether the process comprises a single element. The process is partitioned to determine whether each component satisfies the formula. A plurality of names of the process is determined, and it is verified that a name exists for the formula that is unequal to any of the plurality. Each process sublocation is analyzed, as well as the spatial process reach.
7 Citations
40 Claims
-
1. A computer-implemented method that facilitates ambient calculus-based modal logic model checking, comprising:
-
performing an analysis on an ambient calculus-based representation of a process with a formula that is represented via ambient calculus; and
outputting a result of the analysis that is utilized to facilitate determining whether the process satisfies the formula. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 28)
-
-
12. A computer system that facilitates ambient calculus-based modal logic model checking, comprising:
-
a first component that receives a process for analysis, the process is transformed into an ambient calculus-based representation of the process;
a second component that analyzes the ambient calculus-based representation of the process with an ambient calculus-based representation of a formula via an ambient calculus-based modal logic model checking approach; and
a third component that provides a result of the analysis that includes information related to whether the process satisfies the formula. - View Dependent Claims (13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27)
-
-
29. A method executed on a computer that facilitates model checking via ambient calculus-based modal logic, comprising:
-
matching a received process against a formula via ambient calculus; and
outputting whether the process satisfies the formula, based on the match, the output is utilized to facilitate execution of an action associated with the process. - View Dependent Claims (30, 31, 32, 33, 34, 35, 36, 37)
-
-
38. A data packet transmitted between two or more computer components that facilitates model checking via ambient calculus-based modal logic, comprising:
an ambient calculus-based process that is analyzed against an ambient calculus-based formula, the analysis includes a model checking technique that facilitates determining whether the process satisfies the formula.
-
39. A computer readable medium storing computer executable components that facilitate model checking via ambient calculus-based modal logic, comprising:
-
a component that analyzes a representation of a process based on an ambient calculus model checking approach; and
a component that outputs a result that indicates whether the process satisfies the formula.
-
-
40. A system that facilitate model checking via ambient calculus-based modal logic, comprising:
-
means for representing a received process in an ambient calculus-based form;
means for comparing the ambient calculus-based form of the process with a formula represented in an ambient calculus-based form;
means for determining whether the process satisfies the formula; and
means for providing a corresponding result that facilitates handling the process.
-
Specification