Contact Information:
- Email: tame@itd.nrl.navy.mil
- Phone: (202) 404-8888
- Fax: (202) 404-7942
- U.S. Mail:
- Naval Research Laboratory
Code 5546
4555 Overlook Ave, SW
Washington, DC 20375-5337
- Building Location:
- Building 12, Room 143
- Phone: (202) 404-8888
-
Selected Publications:
2005
"Extended Abstract: Organizing Automaton Specifications to Achieve Faithful Representation." In: Proceedings of the Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'05), Verona, Italy, July 11-14, 2005. PS PDF
This extended abstract describes a general technique for organizing an automaton model of a system (or protocol) that is useful in the context of theorem proving, which we call the reference variable method. In this technique, a (usually complex) reference variable is used to capture the state. In cases when reasoning about the reference variable directly is complicated, auxiliary, shadow variables with provable relationships to the reference variable are used in formalizing properties of the automaton. The shadow variables are updated simultaneously with the reference variable when state transitions occur, and invariants are used to establish the relationships maintained. Proofs of properties relating shadow variables can often be done in an abstraction that omits the reference variable. This technique produces a natural specification in which the connection of the system model to the actual system is clear, and can be useful even when shadow variables are not used. Particularly when shadow variables are used, the technique provides the advantage that different abstractions can be related easily to ensure that they are abstractions of the same system. To illustrate the potential usefulness of the technique, we describe how we applied it in three examples.
"PVS Proof Strategies for Proving Abstraction Properties of Automata". In: Electronic Notes in Theoretical Computer Science, no. 125 (Elsevier, 2005), 45-65. PS PDF
Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the ``natural'' proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation.
2004
"Reusable PVS Proof Strategies for Proving Abstraction Properties of I/O Automata", In: Proceedings of the Fourth International Workshop on Strategies in Automated Deduction (STRATEGIES 2004), July 4, Cork, Ireland, 2004. PostScript, PDF
Recent modifications to PVS support a new technique for defining abstraction properties relating automata in a clean and uniform way. This definition technique employs specification templates that can support development of generic high level PVS strategies that set up the standard subgoals of these abstraction proofs and then execute the standard initial proof steps for these subgoals. In this paper, we describe an abstraction specification technique and associated abstraction proof strategies we are developing for I/O automata. The new strategies can be used together with existing strategies in the TAME (Timed Automata Modeling Environment) interface to PVS; thus, our new templates and strategies provide an extension to TAME for proofs of abstraction. We illustrate how the extended set of TAME templates and strategies can be used to prove example I/O automata abstraction properties taken from the literature.
2003
"Developing User Strategies in PVS: A Tutorial". In: Proceedings of the First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), September 8, Rome, Italy, 2003; available as NASA Proceedings NASA/CP-2003-212448. Proceedings also to appear as an NRL Memorandum Report. PostScript, PDF
This tutorial provides an overview of the PVS strategy language, and explains how to define new PVS strategies and load them into PVS, and how to create a strategy package. It then discusses several useful techniques that can be used in developing user strategies, and provides examples that illustrate many of these techniques.
"Modeling Security-Enchanced Linux Policy Specifications for Analysis", to appear in the Research Summaries for DISCEX III, Washington, DC, April 22-24, 2003. PostScript, PDF
NSA's Security-Enhanced (SE) Linux enhances Linux by providing a specification language for security policies and a Flask-like architecture with a security server for enforcing policies defined in the language. While the security server refers to an internal form of the policy compiled form the policy specification, the description of the policy most understandable to the user is its ``source'' specification in the policy language. It is natural for users to expect to be able to analyze the properties of the policy from this source specification. But the policy language is very low level, making the high level properties of a policy difficult to deduce by inspection. For this reason, tools to help users with the analysis are necessary. The NRL project on analyzing SE Linux policies aims first to use mechanized support to analyze an example policy specification and then to customize this support for use by practitioners in the open source software community. This paper describes how we model policies in the analysis tool TAME, the kinds of analysis we can support, and prototype mechanical support to enable others to model example policies in TAME. The paper concludes with some general observations on desirable properties for a policy language. This paper summarizes the research described in our full paper that is to appear in the proceedings of the IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY 2003), Lake Como, Italy, June 4-6, 2003. The longer paper is also available as NRL Memorandum Report NRL/MR/5540--03-8659.
"Analyzing Security-Enhanced Linux Policy Specifications", NRL Memorandum Report NRL/MR/5540--03-8659. Also to appear in the proceedings of: IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY 2003), Lake Como, Italy, June 4-6, 2003. PostScript, PDF
Security-Enhanced (SE) Linux is a modification of Linux initially released by NSA in January 2001 that provides a language for specifying Linux security policies and, as in the Flask architecture, a security server for enforcing policies defined in the language. To determine whether user requests to the operating system should be granted, the security server refers to an internal form of the policy compiled from the policy specification. Since the most convenient description of the policy for user understanding is its ``source'' specification in the policy language, it is natural for users to expect to be able to analyze the properties of the policy from this source specification. However, though specifications in the SE Linux policy language avoid implementation details, the policy language is very low-level, making the high level properties of a policy difficult to deduce by inspection. For this reason, tools to help users with the analysis are necessary. The goal of the NRL project on analyzing SE Linux security policies is to first use mechanized support to analyze the specification of an example policy, and then to customize this support for use by practitioners in the open source software community. This paper describes how we have modeled an example security policy in the analysis tool TAME, the kinds of analysis we can support, and prototype mechanical support to enable others to model example security policies in TAME. The paper concludes with some general observations on desirable properties for a policy language.
"Developing Strategies for Specialized Theorem Proving about Untimed, Timed, and Hybrid I/O Automata". In: Proceedings of the First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), September 8, Rome, Italy, 2003; available as NASA Proceedings NASA/CP-2003-212448. Proceedings also to appear as an NRL Memorandum Report. PostScript, PDF
In this paper we discuss how we intend to develop a specialized theorem proving environment for the Hybrid I/O Automata (HIOA) framework over the PVS theorem prover, and some of the issues involved. In particular, we describe approaches to using PVS that allow and encourage the development of useful proof strategies, and note some desired PVS features that would further help us to do so for our HIOA environment.
2002
"Towards a Methodology and Tool for the Analysis of Security-Enhanced Linux Security Policies", NRL Memorandum Report 5540--02-8629. PostScript, PDF
Security-Enhanced (SE) Linux, released by NSA in January, 2001, is a version of Linux that adds security features by superimposing the Flask architecture on its kernel. In this architecture, a security server decides whether to grant particular subjects (i.e., processes) permissions to particular objects. The decisions are based on a combination of type enforcement (TE), role-based access control (RBAC), and multilevel security (MLS) rules. SE Linux includes a policy language for defining these parts of the security policy. Because the policy language forces detailed specification of which access permissions may be granted, the relation of a policy definition to high level security goals is not obvious. The length and complexity of policy definitions (thousands of rules is typical) precludes proving a high level security property by inspection. For policy analysis, tool support is clearly needed. To be effective in practice, this tool support needs to be usable by members of the open source software community. This paper reports progress made towards adapting the theorem proving tool TAME to the analysis of SE Linux security policies, and making it usable to open source developers.
"Proving Invariants of I/O Automata with TAME", In Automated Software Engineering, Vol.9, 201-232. PostScript, PDF
This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.
"Stream Authentication Protocol with TAME", Presented at WITS '02, Portland, OR, January 14-15, 2002. PostScript, PDF
The TESLA multicast stream authentication protocol is distinguished from other types of cryptographic protocols in both its key management scheme and its use of timing. It takes advantage of the stream being broadcast to periodically commit to and later reveal keys used by a receiver to verify that packets are authentic, and it uses both inductive reasoning and time arithmetic to allow the receiver to determine that an adversary cannot have prior knowledge of a key that has just been revealed. While an informal argument for the correctness of TESLA has been published, no mechanized proof appears to have previously been done for TESLA or any other protocol of the same variety. This paper reports on a mechanized correctness proof of the basic TESLA protocol based on establishing a sequence of invariants for the protocol using the tool TAME, an interface to PVS specialized for proving properties of automata. It discusses the organization and process used in the proof, and the possibilities for reusing these techniques in correctness proofs of similar protocols, starting with more sophisticated versions of TESLA.
2001Annals of Mathematics and Artificial Intelligence Vol. 29 (2000), No. 1-4, pp. 139-181 (Published February, 2001). PostScript, PDF
TAME (Timed Automata Modeling Environment), an interface to the theorem proving system PVS, is designed for proving properties of three classes of automata: I/O automata, Lynch-Vaandrager timed automata, and SCR automata. TAME provides templates for specifying these automata, a set of auxiliary theories, and a set of specialized PVS strategies that rely on these theories and on the structure of automata specifications using the templates. Use of the TAME strategies simplifies the process of proving automaton properties, particularly state and transition invariants. TAME provides two types of strategies: strategies for ``automatic'' proof and strategies designed to implement ``natural'' proof steps, i.e., proof steps that mimic the high-level steps in typical natural language proofs. TAME's ``natural'' proof steps can be used both to mechanically check hand proofs in a straightforward way and to create proof scripts that can be understood without executing them in the PVS proof checker. Several new PVS features can be used to obtain better control and efficiency in user-defined strategies such as those used in TAME. This paper describes the TAME strategies, their use, and how their implementation exploits the structure of specifications and various PVS features. It also describes several features, currently unsupported in PVS, that would either allow additional ``natural'' proof steps in TAME or allow existing TAME proof steps to be improved. Lessons learned from TAME relevant to the development of similar specialized interfaces to PVS or other theorem provers are discussed.
2000
"Using TAME to Prove Invariants of Automata Models: Two Case Studies", Proc. Third ACM Workshop on Formal Methods in Software Practice (FMSP'00), Portland, OR, August 24-25, 2000, pp. 25-36. PostScript, PDF
TAME is a special-purpose interface to PVS designed to support developers of software systems in proving properties of automata models. One of TAME's major goals is to allow a software developer who has basic knowledge of standard logic, and can do hand proofs, to use PVS to represent and to prove properties about an automaton model without first becoming a PVS expert. A second goal is for a human to be able to read and understand the content of saved TAME proofs without running them through the PVS proof checker. A third goal is to make proving properties of automata with TAME less costly in human time than proving such properties using PVS directly. Recent work by Romijn and Devillers et al., based on the I/O automata model, has provided the basis for two case studies on how well TAME achieves these goals. Romijn specified the RPC-Memory Problem and its solution, while Devillers et al. specified a tree identify protocol. Hand proofs of specification properties were provided by the authors. In addition, Devillers et al. used PVS directly to mechanize the specifications and proofs of the tree identify protocol. In one case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata presented by Romijn and Devillers et al. and to check the hand proofs of invariant properties. The PVS specifications and proofs of Devillers et al. provide the basis for the other case study, which compares the TAME approach to an alternate approach which uses PVS directly.
"Applying TAME to I/O Automata: A User's Perspective". NRL Memorandum Report NRL.MR.5540--00-8848, April 10, 2000. PostScript, PDF
Mechanical theorem provers have been shown to expose proof errors, some of them serious, that humans miss. Mechanical provers will be applied more widely if they are easier to use. The tool TAME (Timed Automata Modeling Environment) provides an interface to the prover PVS to simplify specifying and proving properties of automata models. Originally designed for reasoning about Lynch-Vaandrager (LV) timed automata, TAME has since been adapted to other automata models. This paper shows how TAME can be used to specify and verify properties of I/O automata, a class of untimed automata. It also describes the experiences of a new TAME user (the first author) who used TAME to check Lamport-style hand proofs of invariants for two applications: Romijn's solution to the RPC-Memory Problem and the verification by Devillers et al. of the tree identify phase of the IEEE 1394 bus protocol. For the latter application, the TAME mechanization of the hand proofs of Devillers is compared with the more direct PVS proofs of Devillers et al. Improvements to TAME in response to user feedback are discussed.
1999
SCR: A Practical Approach to Building a High Assurance COMSEC System, Proc. 15th Annual Computer Security Applications Conference (ACSAC '99), IEEE Computer Society Press, December, 1999. To appear. PostScript
To date, the tabular-based SCR (Software Cost Reduction) method has been applied mostly to the development of embedded control systems. This paper describes the successful application of the SCR method, including the SCR* toolset, to a different class of system, a COMSEC (Communications Security) device called CD that must correctly manage encrypted communications. The paper summarizes how the tools in SCR* were used to validate and to debug the SCR specification and to demonstrate that the specification satisfies a set of critical security properties. The development of the CD specification involved many tools in SCR*: a specification editor, a consistency checker, a simulator, the TAME interface to the theorem prover PVS, and various other analysis tools. Our experience provides evidence that use of the SCR* toolset to develop high-quality requirements specifications of moderately complex COMSEC systems is both practical and low-cost.
Applying Formal Methods to an Information Security Device: An Experience Report Proc. 4th IEEE International Symposium on High Assurance Systems Engineering (HASE '99), IEEE Computer Society Press, November, 1999, pp. 81-88. PostScript
SCR (Software Cost Reduction) is a formal method for specifying and analyzing system requirements that has previously been applied to control systems. This paper describes a case study in which the SCR method was used to specify and analyze a different class of system, a cryptographic system called CD, which must satisfy a large set of security properties. The paper describes how a suite of tools supporting SCR---a consistency checker, simulator, model checker, invariant generator, theorem prover, and validity checker---were used to detect errors in the SCR specification of CD and to verify that the specification satisfies seven security properties. The paper also describes issues of concern to software developers about formal methods---e.g., ease of use, cost-effectiveness, scalability, how to translate a prose specification into a formal notation, and what process to follow in applying a formal method---and discusses these issues based on our experience with CD. Also described are some unexpected results of our case study.
Applying Formal Methods to an Information Security Device: A Case Study, Proc. of the Information Systems Technology Panel Symposium on Protecting NATO Information Systems in the 21st Century, Washington, DC, October, 1999. PostScript
One approach to assuring information security is to control access to information through an appropriately designed device. A cost-effective way to provide assurance that the device meets its security requirements is to detect and correct violations of these requirements at an early stage of development: when the operational requirements are specified. Once it is demonstrated that an operational requirements specification is complete and consistent, that it captures the intended device behavior, and that the operational specification satisfies the security requirements, this operational specification can be used both to guide development of implementations and to generate test sets for testing implementations. This paper describes the application of the SCR (Software Cost Reduction) requirements method and the NRL's SCR* toolset, which includes a set of verification and validation tools, to a US Navy communications security device. It reports on our success in proving that the operational requirements specification satisfies a set of security properties. The paper also discusses the practicality and cost of applying formal methods to the development of security devices.
1998
"Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications," IEEE Transactions on Software Engineering, vol. 24, no. 11, November 1998. PostScript, PDF
Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a "practical" formal method, based on this approach and the SCR (Software Cost Reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two "pushbutton" abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification.
"TAME: A PVS Interface to Simplify Proofs for Automata Models," UITP '98, July 1998. PostScript, PDF
Although a number of mechanical provers have been introduced and applied widely by academic researchers, these provers are rarely used in the practical development of software. For mechanical provers to be used more widely in practice, two major barriers must be overcome. First, the languages provided by the mechanical provers for expressing the required system behavior must be more natural for software developers. Second, the reasoning steps supported by mechanical provers are usually at too low and detailed a level and therefore discourage use of the prover. To help remove these barriers, we are developing a system called TAME, a high-level user interface to PVS for specifying and proving properties of automata models. TAME provides both a standard specification format for automata models and numerous high-level proof steps appropriate for reasoning about automata models. In previous work, we have shown how TAME can be useful in proving properties about systems described as Lynch-Vaandrager Timed Automata models. TAME has the potential to be used as a PVS interface for other specification methods that are specialized to define automata models. This paper first describes recent improvements to TAME, and then presents our initial results in using TAME to provide theorem proving support for the SCR (Software Cost Reduction) requirements method, a method with a wide range of other mechanized support.
"Mechanical Verification of Timed Automata: A Case Study," NRL Memorandum Report 5546-98-8180, April, 1998. PostScript, PDF
This report describes the results of a case study on the feasibility of developing and applying mechanical methods, based on the proof system PVS, to prove propositions about real-time systems specified in the Lynch-Vaandrager timed automata model. In using automated provers to prove propositions about systems described by a specific mathematical model, both the proofs and the proof process can be simplified by exploiting the special properties of the mathematical model. Because both specifications and methods of reasoning about them tend to be repetitive, the use of a standard template for specifications, accompanied by standard shared theories and standard proof strategies or tactics, is often feasible. Presented are the PVS specification of three theories that underlie the timed automata model, a template for specifying timed automata models in PVS, and an example of its instantiation. Both hand proofs and the corresponding PVS proofs of two propositions are provided to illustrate how these can be made parallel at different degrees of granularity. Our experience in applying PVS to specify and reason about real-time systems modeled as timed automata is also discussed. The methods for reasoning about timed automata in PVS developed in the study have evolved into a system called TAME (Timed Automata Modeling Environment). A summary of recent developments regarding TAME is provided. A shorter version of the report was presented at the 1996 Real-Time Applications Symposium.
1997
"Human-Style Theorem Proving Using PVS," TPHOLs '97, Murray Hill, NJ, August 19-22, 1997. PostScript, PDF
A major barrier to more common use of mechanical theorem provers in verifying software designs is the significant distance between proof styles natural to humans and proof styles supported by mechanical provers. To make mechanical provers useful to software designers with some mathematical sophistication but without expertise in mechanical provers, the distance between hand proofs and their mechanized versions must be reduced. To achieve this, we are developing a mechanical prover called TAME on top of PVS. TAME is designed to process proof steps that resemble in style and size the typical steps in hand proofs. TAME's support of more natural proof steps should not only facilitate mechanized checking of hand proofs, but in addition should provide assurance that theorems proved mechanically are true for the reasons expected and also provide a basis for conceptual level feedback when a mechanized proof fails. While infeasible for all applications, designing a prover that can process a set of high-level, natural proof steps for restricted domains should be achievable. In developing TAME, we have had moderate success in defining specialized proof strategies to validate hand proofs of properties of Lynch-Vaandrager timed automata. This paper reports on our successes, the services provided by PVS that support these successes, and some desired enhancements to PVS that would permit us to improve and extend TAME.
"Verifying Hybrid Systems Modeled as Timed Automata: A Case Study," Proceedings of HART '97, Grenoble, France, March 26-28, 1997. PostScript, PDF
Verifying properties of hybrid systems can be highly complex. To reduce the effort required to produce a correct proof, the use of mechanical verification techniques is promising. Recently, we extended a mechanical verification system, originally developed to reason about deterministic real-time automata, to verify properties of hybrid systems. To evaluate our approach, we applied our extended proof system to a solution, based on the Lynch-Vaandrager timed automata model, of the Steam Boiler Controller problem, a hybrid systems benchmark. This paper reviews our mechanical verification system, which builds on SRI's Prototype Verification System (PVS), and describes the features we added to handle hybrid systems. It also discusses some errors we detected in applying our system to the benchmark problem. We conclude with a summary of insights we acquired in using our system to specify and verify hybrid systems.
1996
"TAME: A Specialized Specification and Verification System for Timed Automata," Presented in the Work in Progress session at RTSS '96, Washington, D.C., December 4-6, 1996. PostScript, PDF
Assuring the correctness of specifications of real-time systems can involve significant human effort. The use of a mechanical theorem prover to encode such specifications and to verify their properties could significantly reduce this effort. A barrier to routinely encoding and mechanically verifying specifications has been the need first to master the specification language and logic of a general theorem proving system. Our approach to overcoming this barrier is to provide mechanical support for producing specifications and verifying proofs, specialized for particular mathematical models and proof techniques. We are currently developing a mechanical verification system called TAME (Timed Automata Modeling Environment) that provides this specialized support using SRI's Prototype Verification System (PVS). Our system is intended to permit steps in reasoning similar to those in hand proofs that use model-specific techniques. TAME has recently been used to detect errors in a realistic example.
"Mechanical Verification of Timed Automata: A Case Study," Proceedings of the 1996 Real-Time Technology and Applications Symposium, 1996. PostScript, PDF
This paper reports the results of a case study on the feasibility of developing and applying mechanical methods, based on the proof system PVS, to prove propositions about real-time systems specified in the Lynch-Vaandrager timed automata model. In using automated provers to prove propositions about systems described by a specific mathematical model, both the proofs and the proof process can be simplified by exploiting the special properties of the mathematical model. This paper presents the PVS specification of three theories that underlie the timed automata model, a template for specifying timed automata models in PVS and an example of its instantiation, and both hand proofs and the corresponding PVS proofs of two propositions. It concludes with a discussion of our experience in applying PVS to specify and reason about real-time systems modeled as timed automata.
TAME Support for Refinement Proofs
Project Description:
TAME (Timed Automata Modeling Environment) is an interface to PVS for proving properties of both timed and untimed I/O automata. TAME support for mechanized proofs of automaton invariants is well developed, and has been used in many applications. The TAME interface is based on specification templates, supporting theories, and specialized PVS proof strategies. Central to establishing correctness of implementations of automaton specifications is the notion of {\italics refinement}: the implementation refines the specification. This project is aimed at extending the existing TAME interface with appropriate new templates, theories, and strategies in order to support mechnanized proofs of refinement relations between automata.
Principal Investigator: Myla Archer
Sponsor: CNO/ONR