Transcript CTR-S: A Logic for Specifying Contracts in Semantic Web Services

AS3: Adaptive, Situation-Aware and
Secure Service-Based Systems
Hasan Davulcu
Department of Computer Science and Engineering
Arizona State University
Joint work with:
Dr. Stephen S. Yau
Dr. Supratik Mukhopadhyay
MURI Review Meeting, June, 2005
1
Outline

Introduction and Examples

Our research goals on AS3 systems

AS3 Calculus and Logic

Secure and Adaptive Workflow Synthesis

Conclusion and future work
MURI Review Meeting, June, 2005
2
Introduction

Service-based systems (SBS):

Systems offering services which are well-defined
functions used in different contexts and have
interrelations and dependencies



Services are not restricted to Web services
Individual services are usually independently
designed and implemented, and run on loosely
coupled systems
Examples:



Emergency response information systems
e-Business
…
MURI Review Meeting, June, 2005
3
An Example of SBS
- Road Emergency Response
Workflow
Planning
& Scheduling
Accident Report
AMS
Passenger
in critical
condition
Send
Patrol Car
AMB
Setup
Perimeter
CAR
L
Police Dept.
(PD)
H
FE
Fire Dept.
(FD)
MURI Review Meeting, June, 2005
4
Coordination Constraints




All the responders should arrive at the accident site
within fifteen minutes.
Any CAR, FE, AMB, or H that are serving at one
accident site should not be dispatched to another
accident site before completing their jobs at the
accident site.
Injured passengers in critical conditions should be
brought to a nearby hospital within fifteen minutes
after they are rescued from their damaged vehicles.
Any coordination agent should only follow the
commands from a trusted MP, being authenticated
and delegated by a trusted party (the proper
authority). Only after CARs leaves from L, ERC can
end the road closure.
MURI Review Meeting, June, 2005
5
Dynamic reconfiguration
Constraints

Since, it is almost impossible to identify all control and correction
steps before execution time, the system must provide the capability to
adapt the workflows at run-time with dynamic reconfiguration
constraints:



Resource failure: An ambulance can transport at most two injured
passengers at the same time, and hence the MP should send another
ambulance within five minutes to carry additional injured passengers.
Service failure: If the police fail to set up a perimeter within fifteen
minutes after the 911 call center gets an accident report, FE and AMB
can enter the accident site regardless a police perimeter has been set
up or not.
Exception Condition: If the paramedics determine that one of the
injured passengers is in critical condition then, another helicopter (H1)
is discovered and used to transport the passenger in critical condition
to the hospital.
MURI Review Meeting, June, 2005
6
Requirements

Adaptability



System adaptation to provide acceptable performance
in spite of system failures, overload, or damages
Rapid reconfiguration to achieve users’ new missions
Security



Authentication for both users and service providers
Protection of critical information and critical operations
of distributed services
Enforcement of flexible security policies of distributed
services from joint/coalition operations
MURI Review Meeting, June, 2005
7
Objective of Our Project

Conduct basic research on generating techniques for
rapid development, deployment and operations of AS3
Systems with high confidence and cost-effectiveness.
1. Hierarchical situation-awareness capability.
2. Distributed trust management to ensure policy-based
security.
3. Rapidly discovering, contracting with and composing
reliable and unreliable services into processes with
situational and QoS constraints
4. Adapting these processes when situations, mission
goals and/or security policies change
MURI Review Meeting, June, 2005
8
Our Approach

Provide a declarative unifying logic-based approach for
extending service-oriented architecture with:



Hierarchical situation-awareness for reactive behavior
Distributed trust management for managing and
enforcing security policies
Adaptive workflow management for deliberative actions,
which are composed and coordinated automatically to
achieve users’ goals
while preserving overall correctness and consistency.
MURI Review Meeting, June, 2005
9
AS3 System Architecture
Fe
ed
ba
ck
Formal Specification
of Mission Goals
Security
Agents
(SeA)
Workflow
SituationAwareness
Agents
(SAA)
Services
MURI Review Meeting, June, 2005
10
Major Components of
Our Approach
AS3 Calculus and Logic
II. Distributed trust management
III. Adaptive workflow synthesis
IV. Distributed workflow scheduling
I.
MURI Review Meeting, June, 2005
11
Our Approach to Rapid
Development of AS3 Systems
AS3 System specifications
AS3 Logic
(I)
Service
specs
(IV)
QoS specs
H-SAW Security Real-time
(II)
(V)
policies
(III)
Application
independent
properties
Mission goal
spec
(IV)
Adaptive workflow synthesis (IV)
Dynamic
Model and Type Model-based Diagnosis
Proof System
Checker
and Recovery
AS3 Calculus
(I)
Workflow
H-SAW Agents
Security Agents
(II)
(III)
Distributed workflow
scheduler
(V)
Online Fault Management
for Hierarchical SAW
Agents
(II)
Compiler
SINS Virtual Machine
MURI Review Meeting, June, 2005
12
Existing Standards for Servicebased Systems
BPEL/BPEL4WS [21]: Industry standard
1.



For modeling and executing workflows
Lacks formal semantics
Does not provide automatic service composition and
adaptation
OWL-S, Web Components [36]:
2.



Provides constructs for unambiguously describing the
properties and capabilities of Web services
Provides limited formal guarantees
Does not provide automatic service composition
MURI Review Meeting, June, 2005
13
Existing Formal Approaches

Rule-based Modeling (SWORD) [28]:



Classical Process Calculi and Synchronous
Programming Languages:




Does not allow services having side effects
Currently, no work is known that uses SWORD for modeling
situation-awareness or security policies
Pi calculus [33,34], Ambient Calculus [32], Chemical Abstract
Machine [35]: Does not provide facilities for processing
situation information and reacting to it
SOL [37]: Does not provide facilities for automatic service
composition
Provides ways for formal reasoning
Linear Logic [29]:

Undecidable: provides only semi-automated service
composition
MURI Review Meeting, June, 2005
14
A Simple Example
Enemy
Exec: ShipA.Missile
ShipA.Radar
lockmissile
fire
enemy
Monitoring Agent
Enemy detected
ShipA
ShipB
Commander
MURI Review Meeting, June, 2005
15
Our




Calculus
Provides a formal programming model for AS3
systems
Is based on classical process calculi, and has
operational semantics involving interactions
between:


3
AS
external actions: communication, leaving and
joining groups
internal computations: method calls of named
services
Can model timeouts and failures
Implements access control using hierarchical
domains
MURI Review Meeting, June, 2005
16
A Calculus for AS3 Systems
(System)
(Process)
P::=
S::=
(new n) P
fix I=P (recursion)
0
N[S] (named
P||P
domain)
I
S||S (Sys. Comp.)
E.P
N ::=
x (variable)
n (name)
(name restriction)
(inactive process)
(par. composition)
(identifier)
(external action)
C.P (int. computation)
P1+P2 (nondet. choice)
fail (failure)
catch(n).P (failure handler)
time t.P (timeout)
P{l1(x1),…;…ln(xn)} (method
export)
 External action involves communication, leaving or joining groups, removing firewalls
 Internal computation takes place by calling methods of identified services
MURI Review Meeting, June, 2005
17
External Actions
E ::=
M (Domain)
K (Comm.)
K::=
(comm.)
(x) (input)
<Z> (output)
M ::=
in N (enter a
dom.)
out N (exit a dom.)
open N (open
firewall)
M.M’ (concat)
ε (no action)
MURI Review Meeting, June, 2005
18
Internal Computation
C::=
Let x=C instantiate P
if C(x) then P else P’
I:li(y)
service)
I:li ← I’:lj
ρ
C.C
ε
true
false
⊥
I:li=
(beta reduction)
(conditional)
(method invocation for identified
(method replacement)
(constraint evaluation)
(concatenation)
(no-computation)
(constant true)
(constant false)
(failed computation)
pre::post(xi)
MURI Review Meeting, June, 2005
19
Security Model

An AS3 system is secure iff only two
entities (processes) in the same domain
can communicate.


When two entities are not in the same
domain, they must move into the same
domain for communication
Security (access control) model
synthesized through formula rewriting
using sound transformation rules in AS3
logic
MURI Review Meeting, June, 2005
20
Security Model (cont.)
n
m
A
B
 Is A allowed to communicate with B?
--Is A currently authenticated to n ?
--Can A currently move out from m to n to
communicate with B ?
MURI Review Meeting, June, 2005
21
3
AS
Processes for the Example
System
ShipB
ShipA
Monitoring Agent
Commander
Fleet
Fleet =
if MA:detect_intrusion() then
let <x,y>=MA:
get_enemy_coordinates() instantiate
<x,y>.MA
else
MA
(x,y). In
fleet.<x,y>.<destroy>.
out fleet.CMD
fleet[shipA || shipB]
shipA= (x,y).(d).
if d=“destroy” then
(shipA:lock_radar(x,y).shipA:load_missile().(let
z=shipA:fire()
instantiate if z=
enemy_destroyed then <z> ) then shipA)
else
shipA
shipB ≌ shipA
MURI Review Meeting, June, 2005
22
AS3 Processes for the Example
(cont.)
Enemy
Monitoring Agent
if MA:detect_intrusion() then
let <x,y>= MA: get_enemy_coordinates()
instantiate <x,y>
MA
else
MA
MURI Review
Meeting, June, 2005
Commander
23
AS3 Processes for the Example
(cont.)
Commander
(x,y). In fleet.
<x,y>.<destroy>
<x,y>.<destroy>.
out fleet.CMD.
ShipA
ShipB
MURI Review Meeting, June, 2005
Fleet
24
AS3 Processes for the Example
(cont.)
Enemy
enemy destroyed
ShipA
ShipB
Fleet
Fleet = fleet[shipA || shipB]
shipA= (x,y).(d).
if d=“destroy” then
shipA:lock_radar(x,y)
shipA:load_missile()
let z=shipA:fire() instantiate if z= enemy_destroyed then <z> then
shipA
else
shipA
MURI Review Meeting, June, 2005
25
Synthesis of AS3 Processes

Can we synthesize AS3 processes
automatically from declarative
specifications?

Yes, use our approach
MURI Review Meeting, June, 2005
26
Our Approach: Logic-based
Synthesis of AS3 Processes
1.
2.
3.
4.
Services described in AS3 logic along with
proof rules of the logic form a theory of
AS3 systems
Functional requirements of the mission
along with QoS (real-time, security,
situation-awareness) described as formulae
in AS3 logic
Synthesis amounts to a proof of the
requirements using the AS3 theory
Executable calculus terms directly
synthesized from the proof
MURI Review Meeting, June, 2005
27
Our AS3 Logic

Modal Logic talking about both time and
space



Sometime modality for temporal evolution,
somewhere modality for spatial location
Modalities for communication, leaving
joining domains, knowledge
Atomic formulas for describing relations
among variables
MURI Review Meeting, June, 2005
28
AS3 Logic Syntax
φ ::=
0
pred(x1,…,xn)
t~c
φ1∨φ2
┐φ
◊φ
Θφ
I
(inactivity)
(user defined atoms)
(atomic constraint)
(disjunction)
(negation)
(sometime)
(somewhere)
(identifier/nominal match)
~::=> | <| ≤| ≥
c: Natural Number
MURI Review Meeting, June, 2005
29
AS3 Logic Syntax (Contd.)
φ1|| φ2
η[φ]
φ@η
K(u; φ)
serv(u; φ)
n φ
t φ
in(n) φ
(parallel composition)
(named domain)
(behavior within domain)
(knowledge of an object)
(recording of an object)
(quantification over names)
(quantification over real variables)
(behavior after entering
domain)
out(n) φ
(behavior after leaving
domain)
<u> φ
T
(behavior after sending message)
(constant true)
MURI Review Meeting, June, 2005
30
AS3 Logic: Properties
 Decidable when interpreted over
systems with image-finite processes
 Model checking problem is also
decidable for systems with image-finite
processes
MURI Review Meeting, June, 2005
31
Proof Theory of AS3 Logic

All axioms of propositional modal
logic and the following axioms:
T1: Θ(σ || n[φ])  next_hierarchy(σ,φ)
T2: next_hierarchy(φ,σ)→Θσ
T3: Θ◊φ→◊Θφ
T4: φ→Θφ
T5: ΘΘφφ
MURI Review Meeting, June, 2005
32
Transformation Rules for
Synthesis of Access Control
Security (access control) model synthesized
through formula rewriting using sound
transformation rules in AS3 logic
A1: restrict(I,φ)  ┐Θ(I ||φ)
A2: restrict(I,J) ∧ Θ(J || K) →┐Θ(I || K)
and 7 other transformation rules for synthesis of
access control
MURI Review Meeting, June, 2005
33
The Simple Example in AS3 Logic
Entities: (Nominals/Identifiers)
shipA, shipB, MA, CMD
Goal:
R1: detect_intrusion(MA)
→◊Θserv(“enemy_destroyed”; T)
If the MA detects an intrusion then eventually
somewhere there will be a process that will
record “enemy_destroyed”
MURI Review Meeting, June, 2005
34
Service Coordination Descriptions in
AS3 Logic
S1:
detect_intrusion(MA)
→ ◊serv(“enemy_ship”; MA)
S2:
serv(“enemy_ship”;MA)
→◊get_coordinates(u,v;MA)
S3: get_coordinates(u,v;MA)
→◊ serv(u,v;MA)
and two other axioms
MURI Review Meeting, June, 2005
35
Access Control Requirement:
The Simple Example

Only CMD is allowed to communicate to shipA or
shipB

MA cannot directly communicate with shipA or shipB
AC1:
U=shipA  U=shipB →□restrict(MA,U)
AC2:
System[MA || T]
AC3:
□┐restrict(shipA,shipB)
AC4:
┐restrict(CMD, MA)
MURI Review Meeting, June, 2005
36
Deductive Proof and Process
Synthesis
AC4
A3
AC2
T4
(1) ┐restrict(CMD, MA) …(AC4)
(2) ┐restrict(I,σ)→Θ(I||σ) … (A3) … (A3)
(3)
A4
(6)
(3) Θ(MA || MA) … (MP…
1,2)
(MP 1,2)
(4) System[MA|| T]
… (AC2)
(8) AC1 AC3
A5
(5) φ→Θφ
… (T4)
(6) Θ System[MA || T]
… (Sub. 4, 5)
(12)
A9
(7) Θn[σ || ρ] /\ Θ(φ || σ)→ Θ n[φ || σ || ρ] … (A4)
(8) Θ
CMD
|| T]|| T]
…(MP
4,6,7) 4,6,7)
(8)
ΘSystem[MA||
System[MA||
CMD
…(MP
(9) restrict(shipA, MA)
…(AC1)
(14)
(10) □┐restrict(shipA,shipB)
…(AC3)
(11) restrict(φ,σ) /\ ┐restrict(φ,ρ)→restrict(φ || ρ,σ)
…(A5)
(1) ┐restrict(CMD, MA) …(AC4)
(2) ┐restrict(I,σ)→Θ(I||σ) … (A3)
(4)
T]
… (MP
(AC2)
(3) System[MA||
Θ(CMD || MA)
1,2)
(5) φ→Θφ
… (T4)
(7)
|| ρ] /\ Θ(φ|| T]
|| σ)→ …
Θ n[φ
|| σ4,||5)
ρ] … (A4)
(6) Θn[σ
Θ System[MA
(Sub.
(8)
Θ System[MA||MA)
CMD || T]
…(MP 4,6,7)
(9) restrict(shipA,
…(AC1)
(10) □┐restrict(shipA,shipB)
…(AC3)
(12)
… (MP 9,10,11)
(11)restrict(shipA||shipB,MA)
restrict(φ,σ) /\ ┐restrict(φ,ρ)
(13) Θn[φ||J]  restrict(K,J)→Θn[φ||m[K]||J]  Θ(n[φ||J] || m[K]) …(A9)
→restrict(φ || ρ,σ)
…(A5)
(14) Θ System[CMD|| MA || m[shipA||shipB] || T] (MP 8,12,13)
(12) restrict(shipA||shipB,MA)
… (MP 9,10,11)
MURI Review Meeting, June, 2005
37
Deductive Proof and
Process Synthesis
Goal: R1: detect_intrusion(MA)
→◊Θserv(“enemy_destroyed”; T)
S1:
fix MA=
detect_intrusion(MA)→
let x=MA:detect_intrusion()
◊serv(“enemy_ship”; MA)
Instantiate
S2:
if x=“enemy_ship” then let
serv(“enemy_ship”;MA)
(u,v)=MA:get_coordinates()
→◊get_coordinates(u,v; instantiate
MA)
…
…
MURI Review Meeting, June, 2005
38
Demo of Static Proof
Theory …
MURI Review Meeting, June, 2005
39
Image Finiteness of Processes

We impose the following restrictions on
processes





Recursive processes are guarded
Parallel composition through recursion is not
allowed (similar to Pi-calculus [Dam 93])
A type system can check for well-formedness
of processes
Image Finiteness: A closed process term can
only evolve (in zero or more steps) into
finitely many non-congruent process terms
using the reduction rules
Restrictions ensure that every process is
image finite
Back
MURI Review Meeting, June, 2005
40
Semantics of AS3 Logic
Interpreted over systems decorated with
atomic formulas
P ╞ I if fix I=P
P ╞ <u> φ if there exists Q, R,S,T P≌<u>Q,

R ≌ (x).S,T= P||R and Q╞ φ
P ╞ pred(u1,…,un) if P is decorated with
pred(u1,…,un)
P ╞ in(n) φ if there exists Q, n, R, S, P ≌ in
n.Q, Q╞ φ @n, S ≌ P || n[R]
Back
MURI Review Meeting, June, 2005
41
Transformation Rules for
Access Control (Cont.)
A3: ┐restrict(I,σ)→Θ(I ||σ)
A4: Θn[ρ || σ] ∧ Θ(φ || σ)→Θn[φ || σ || ρ]
A5: restrict(φ,σ)∧┐restrict(φ,ρ)→restrict(φ || ρ,σ)
A6: next_hierarchy(I,σ)→restrict(I,σ)
A7: restrict(I,σ) /\ Θ(I || J)→restrict(J,σ)
A8: restrict(σ,φ)→restrict(φ,σ)
A9: Θn[φ || J] /\ restrict(K,J)→Θn[φ ||m[K] || J] V Θ(n[φ || J] || m[K])
[Back]
MURI Review Meeting, June, 2005
42
Service Descriptions in AS3
Logic
S4:
serv(u,v;MA)→◊K(u,v;CMD)
S5:
K(u,v;CMD)→◊K(u,v;shipA)\/◊K(u,v;ship
B)
Back
MURI Review Meeting, June, 2005
43
Policy Enforcement: Model-based
Diagnosis and Recovery




System was synthesized based on the
assumption that services do not behave
maliciously: Unrealistic assumption
Runtime enforcement ensures diagnosis of
malicious behavior on the part of services and
subsequent recovery
Service specifications used to generate
symptoms
Abduction based diagnosis uses the models
(process terms) to diagnose breach of trust
by services and ensure recovery
MURI Review Meeting, June, 2005
44
Requirements of AS3 Systems

Adaptability



Security



Provide acceptable performance in the presence of
system failures, overload, or damages
Rapid reconfiguration to achieve users’ new missions
Authentication for both users and service providers
Protection of critical information infrastructure of
distributed services based on flexible security policies
 For example, access control requirements
Situation-Awareness (SAW) – capability of being
aware of complex situations for
 Service coordination


Adapting workflows when situations change
Enforcing situation-aware
security
MURI Review Meeting,
June, policies
2005
45
A Simple Example

A simplified version of the ship scenario
in the overview slides




Intrusion of enemy detected by Monitoring
Agent that reports to the CMD
The CMD directly asks shipA (or shipB) to
destroy the enemy ship rather than
sending a warning
We assume no failures take place
The Combat System Agent has been
eliminated
MURI Review Meeting, June, 2005
46
AS3 Processes for the Example
System = MA || CMD || fleet [shipA || shipB]
fix MA =
if MA: detect_intrusion() then
let <x,y>= MA: get_enemy_coordinates()
<x,y>.MA
else
MA
instantiate
fix CMD =
(x,y). in fleet.<x,y>.<destroy>.out fleet.CMD
fix shipA= (x,y).(d).
if d=“destroy” then
(shipA:lock_radar(x,y).shipA:load_missile().(let z=shipA:fire()
instantiate if z= enemy_destroyed then <z> ) then shipA)
else
shipA
shipB ≌shipA
MURI Review Meeting, June, 2005
47
Synthesis of AS3 Processes



Security (access control) model
synthesized through formula rewriting
using sound transformation rules in AS3
logic
Service specifications including QoS
properties axiomatized in AS3 logic
Functional as well as QoS goals of a
mission expressed in AS3 logic
MURI Review Meeting, June, 2005
48
Papers, Theses and Reports
Publications resulted from AS3 project

[1] S. S. Yau, H. Davulcu, S. Mukhopadhyay, D. Huang and Y. Yao,
"Adaptable Situation-Aware Secure Service Based Systems", Proc. 8th
IEEE Int'l Symp. on Object-oriented Real-time distributed Computing
(ISORC2005), May 2005, pp.308-315.
[2] S. S. Yau, Y. Yao, Z. Chen and L. Zhu, “An Adaptable Security
Framework for Service-based Systems,” Proc. 10th IEEE Int’l
Workshop on Object-oriented Real-time Dependable Systems
(WORDS2005), February 2005, pp. 28-35.
[3] S. S. Yau, D. Huang, H. Gong and H. Davulcu, “Situation-Awareness
for Adaptable Service Coordination in Service-based Systems”, Proc.
29th Annual Int'l Computer Software and Application Conference
(COMPSAC 2005), September 2005, to appear.
[4] S. S. Yau and D. Huang, “Mobile Middleware for Situation-Aware
Service Discovery and Coordination”, Mobile Middleware, edited by
Paolo Bellavista and Antonio Corradi, 2005, Chapter 5.g, to appear.
MURI Review Meeting, June, 2005
49
References
(check against references in MURI book chapter)
[Abe04] D. Aberdeen, S. Thiébaux, L. Zhang. Decision-Theoretic Military Operations Planning. In
ICAPS-04, 2004.
[Bac01] F. Bacchus and M. Ady, Planning with Resources and Concurrency: A Forward Chaining
Approach, International Joint Conference on Artificial Intelligence (IJCAI-2001), pages 417-424,
2001.
[Bly93] Jim Blythe and W. Scott Reilly, “Integrating Reactive and Deliberative Planning in a
Household Robot”, Technical Report CMU-CS-93-155, Carnegie Mellon University, School of
Computer Science, May 1993.
[Bon01] A. Bonifati, S. Ceri, and S. Paraboschi. Pushing reactive services to XML repositories using
active rules. In Proc. 10th World-Wide-Web Conference, 2001.
[Bon03] B. Bonet and H. Geffner. Labeled RTDP: Improving the Convergence of Real Time Dynamic
Programming. 13th International Conference on Automated Planning and Scheduling (ICAPS2003), Trento, Italy, June 2003.
[Bro91a] Rodney Brooks, "Integrated systems based on behaviors", In Proceedings of AAAI Spring
Symposium on Integrated Intelligent Architectures, Stanford University, March 1991. Available
in SIGART Bulletin, Volume 2, Number 4, August 1991.
[Bro91b] Rodney Brooks, “Intelligence without reason”, In Proc. of IJCAI-91. Morgan Kaufmann,
San Mateo, 1991.
[Cha87] David Chapman. "Planning for conjunctive goals", Artificial Intelligence, 32:333–378, 1987.
[Dav94] Davidsson, P., "Concepts and autonomous agents", LU--CS--TR: 94--124, Department of
computer science, Lund University, 1994
[Den03]G. Denker, L. Kagal, T. W. Finin, M. Paolucci, and K. P. Sycara. Security for DAML web
services: Annotation and matchmaking. In International Semantic Web Conference,2003, pp.
335-350.
[Dor97] J. E. Doran, et al, "On Cooperation in Multi-Agent Systems", The Knowledge Engineering
Review, 12(3), 1997.
[Feo95] T.A. Feo and M.G.C. Resende, “Greedy randomized adaptive search procedures,” Journal of
Global Optimization, vol. 6, 1995, pp. 109--133.
MURI Review Meeting, June, 2005
50
References (cont.)
[Fur02] D. Furcy S. Koenig and C. Bauer. Heuristic search-based replanning. In Proceedings of the
International Conference on Artificial Intelligence Planning and Scheduling, 2002.
[Gar02] A.Garland and N. Lesh, Continuous Plan Evaluation with Incomplete Action Descriptions, Proc.
3rd Int'l NASA WS on Planning and Scheduling for Space, Houston, TX, 2002.
[Gil04] Yolanda Gil, Ewa Deelman, Jim Blythe, Carl Kesselman and Hongsuda Tangmunarunkit, “Artificial
Intelligence and Grids: Workflow Planning and Beyond”, IEEE Intelligent Systems, special issue on escience, Jan/Feb 2004.
[Liu04] Y. Liu S. Koenig, M. Likhachev and D. Furcy. Incremental heuristic search in artificial intelligence.
Artificial Intelligence Magazine, 2004 (in press).
[Lu02] Chenyang Lu, John A. Stankovic, Gang Tao and Sang H. Son, "Feedback Control Real-Time
Scheduling: Framework, Modeling, and Algorithms," Real-Time Systems Journal, vol. 23(1/2), 2002,
pp. 85-126.
[Kro03] R. van der Krogt, M. de Weerdt, and C. Witteveen. A resource based framework for planning and
replanning. Web Intelligence and Agent Systems, 1(3/4):173-186, 2003.
[Kro04] R. van der Krogt and M. de Weerdt. The two faces of plan repair. In Proceedings of the Sixteenth
Belgium-Netherlands Conference on Artificial Intelligence (BNAIC-04), pages 147-154, 2004.
[Nam01] Brian Mac Namee, Pádraig Cunningham, "A Proposal for an Agent Architecture for Proactive
Persistent Non Player Characters", Proceedings of the Twelfth Irish Conference on Artificial
Intelligence and Cognitive Science pp. 221-232, 2001.
[Nie03] Niederberger C., Gross M. , "Hierarchical and Heterogeneous Reactive Agents for Real-Time
Applications", Computer Graphics Forum, September 2003, vol. 22, no. 3, pp. 323-331
[Nou97] Nourredine Bensaid and Philippe Mathieu, "A hybrid architecture for hierarchical agents", pages
91-95. Griffith University, Gold-Coast, Australia, February 1997.
[Nwa96] Hyacinth S. Nwana, "Software Agents: An Overview", Knowledge Engineering Review, Vol. 11,
No 3, pp. 205-244, October/November 1996.
[Res02] M. G. C. Resende and C. C. Ribeiro. Greedy randomized adaptive search procedures. In F. Glover
and G. Kochenberger, editors, Handbook of Metaheuristics, pp. 219-249. Kluwer, 2002.
MURI Review Meeting, June, 2005
51
References (cont.)
[Sen02] P. Senkul, M. Kifer, and I. H. Toroslu, “A Logical Framework for
Scheduling Workflows under Resource Allocation Constraints,” Proc. 28th Int’l
Conf. on Very Large Data Bases (VLDB’02), 2002, pp. 694-705.
[Urd03] C. Urdiales, et al, "Hierarchical planning in a mobile robot for map
learning and navigation", in Autonomous Robotic Systems - Soft Computing
and Hard Computing Methodologies and Applications, D. Maravall, D. Ruan
and C. Zhou (eds), Springer Verlag Pub pp. 165-188, 2003
[Vas04] Vasco Pires, Miguel Arroz, Luis Custódio, Logic Based Hybrid Decision
System for a Multi-robot Team, 8th Conference on Intelligent Autonomous
Systems, Amsterdam, The Netherlands, 2004
[Woo02] Mike Wooldridge, "An Introduction to Multiagent Systems by Michael
Wooldridge", ISBN 0 47149691X, John Wiley & Sons (Chichester, England),
February 2002
[Wu03] D. Wu, B. Parsia, E. Sirin, J. Hendler, and D. Nau. Automating DAML-S
web services composition using SHOP2. Proceedings of the Second
International Semantic Web Conference (ISWC2003), November 2003.
MURI Review Meeting, June, 2005
52
SINS and SOL

SINS (Secure Infrastructure for Networked Systems)





An agent-based middleware
Comprise SINS Virtual Machines for instantiating agents
SVMs communicate using Agent Control Protocol
Agents are specified using SOL and can be automatically generated
and verified
SOL (Secure Operation Language)





A synchronous programming language
SOL is secure
SOL programs are amenable to fully automated static analysis
techniques, such as automatic theorem proving using decision
procedures or model checking
SOL has the ability to express a wide class of enforceable safety and
security policies
A set of design and analysis tools, including visual representation tool,
verification tools and interpreters to other languages, are available for
SOL
[Back]
MURI Review Meeting, June, 2005
53
Equational Theory


An equational theory for AS3 calculus is provided by the
structural congruence relation defined below. It allows
syntactic identification of two processes having identical
behavior
A process is structurally congruent to its alpha-renamed
variant
If P≌Q then
1.
C.P ≌ C.Q
2.
A.P ≌ A.Q
3.
P||R ≌ Q||R
4.
R||P ≌ R||Q
5.
N[P] ≌ N[Q]
6.
(new n) P ≌ (new n) Q
7.
fix I=P ≌ fix I=Q
8.
P+R ≌ Q+R
[Back]
MURI Review Meeting, June, 2005
54
Normal Hybrid Modal Logic


“A normal modal logic  is a set of formulas that contains all
tautologies, □(→), (□→□), and ◊□, and is
closed under uniform substitution, modus ponens, and
generalization” [Blackburn]
“Hybrid logics use one sort of atoms called nominals to refer to
states which are regarded as first class citizens” [Blackburn]
[Back]
MURI Review Meeting, June, 2005
55