Current Issue | Faculty of Computer Science

Volume XXII, Issue 2, 2012

Indirect Jumps Improve Instruction Sequence Performance, pages 253-265

J.A. Bergstra, C.A. Middelburg

Abstract | Full text | BibTeX | References | Article page

Instruction sequences with direct and indirect jump instructions are as expressive as instruction sequences with direct jump instructions only. We show that, in the case where the number of instructions is not bounded, we are faced with increases of the maximal internal delays of instruction sequences on execution that are not bounded by a linear function if we strive for acceptable increases of the lengths of instruction sequences on elimination of indirect jump instructions.

Keywords: instruction sequence performance, indirect jump instruction, maximal internal delay

DOI: 10.7561/SACS.2012.2.253

[1] J. A. Bergstra and M. E. Loots. Program algebra for sequential code. Journal of Logic and Algebraic Programming, 51(2):125-156, 2002. http://dx.doi.org/10.1016/S1567-8326(02)00018-8 .

[2] J. A. Bergstra and C. A. Middelburg. Instruction sequences with indirect jumps. Scientic Annals of Computer Science, 17:19-46, 2007.

[3] J. A. Bergstra and C. A. Middelburg. Instruction sequence notations with probabilistic instructions. arXiv:0906.3083v1 [cs.PL], June 2009.

[4] J. A. Bergstra and C. A. Middelburg. On the expressiveness of single-pass instruction sequences. Theory of Computing Systems, 50(2):313-328, 2012. http://dx.doi.org/10.1007/s00224-010-9301-8 .

[5] J. A. Bergstra and A. Ponse. Combining programs and state machines. Journal of Logic and Algebraic Programming, 51(2):175-192, 2002. http://dx.doi.org/10.1016/S1567-8326(02)00020-6 .

[6] J. A. Bergstra and M. B. van der Zwaag. Mechanistic behavior of single- pass instruction sequences. arXiv:0809.4635v1 [cs.PL], September 2008.

[7] J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specication. Addison-Wesley, Reading, MA, second edition, 2000.

[8] A. Hejlsberg, S. Wiltamuth, and P. Golde. C# Language Specication. Addison-Wesley, Reading, MA, 2003.

[9] S. H. P. Schroevers. Expressiveness and extensions of an instruction sequence semigroup. arXiv:1003.1572v1 [cs.PL], March 2010.

Standard Type Soundness for Agents and Artifacts, pages 267-326

F. Damiani, P. Giannini, A. Ricci, M. Viroli

Abstract | Full text | BibTeX | References | Article page

Formal models, core calculi, and type systems, are important tools for rigorously stating the more subtle details of a language, to characterise and study its features and the correctness properties of its programs. In this paper we present {FsimpAL} (FsimpaALlong), a formal calculus modelling the agent and artifact program abstractions provided by the simpA{} agent framework. The formalisation is largely inspired by textsc{Featherweight Java}. It is based on reduction rules applied at certain evaluation contexts, properly adapted to the concurrency nature of simpA{}. On top of this calculus we introduce a standard type system and prove its soundness, so as to guarantee that the execution of a well-typed program does not get stuck. Namely, all primitive mechanisms of agents (activity execution), artifacts (field/property access and step execution), and their interaction (observation and invocation) are guaranteed to be used in a way that is structurally compliant with the corresponding definitions: hence, there will not be run-time errors due to {FsimpAL} distinctive primitives.

Keywords: multi-agent systems, concurrency, type systems

DOI: 10.7561/SACS.2012.2.267

[1] M. Abadi and L. Cardelli. A Theory of Objects. Springer, 1996.

[2] Gul Agha. Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge, MA, USA, 1986.

[3] Gul Agha, Peter Wegner, and Akinori Yonezawa, editors. Research directions in concurrent object-oriented programming. MIT Press, Cambridge, MA, USA, 1993.

[4] Joe Armstrong. Erlang. Commun. ACM, 53:68-75, September 2010. http://dx.doi.org/10.1145/1810891.1810910 .

[5] Fabio Luigi Bellifemine, Giovanni Caire, and Dominic Greenwood. De- veloping Multi-Agent Systems with JADE. Wiley, 2007.

[6] Nick Benton, Luca Cardelli, and Cedric Fournet. Modern concurrency abstractions for C#. ACM Trans. Program. Lang. Syst., 26(5):769-804, 2004. http://dx.doi.org/10.1145/1018203.1018205 .

[7] R. H. Bordini, M. Dastani, J. Dix, and A. El Fallah Seghrouchni, editors. Multi-Agent Programming: Languages, Platforms and Applications (vol. 2). Springer, 2009.

[8] Rafael Bordini, Mendi Dastani, Jurgen Dix, and Amal El Fallah Seghrouchni, editors. Multi-Agent Programming: Languages, Platforms and Applications (vol. 1). Springer, 2005.

[9] Rafael Bordini, Jomi Hubner, and Mike Wooldridge. Programming Multi-Agent Systems in AgentSpeak Using Jason. John Wiley & Sons, Ltd, 2007.

[10] Jean-Pierre Briot, Rachid Guerraoui, and Klaus-Peter Lohr. Concurrency and distribution in object-oriented programming. ACM Comput. Surv., 30(3):291-329, 1998. http://dx.doi.org/10.1145/292469.292470.

[11] Tony Clark. Specication and implementation of a multi-agent calculus based on higher-order functions. Technical report, Department of Computing, University of Bradford, 1999.

[12] J-L. Colaco, M. Pantel, and P. Sall. CAP: An actor dedicated process calculus. In In the ECOOP96 Workshop on Proof Theory of Concurrent Object-Oriented Programming (PTCOOP96), 1996.

[13] Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. On Re-classication and Multi-threading. Journal of Object Technology (www.jot.fm), 3(11):5-30, 2004. http://dx.doi.org/10.5381/jot.2004.3.11.a1 .

[14] Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Re-classication and multi-threading: FickleMT. In Proceedings of the 2004 ACM symposium on Applied computing, SAC '04, pages 1297-1304, New York, NY, USA, 2004. ACM. http://dx.doi.org/10.1145/967900.968163 .

[15] Ferruccio Damiani, Elena Giachino, Paola Giannini, and Emanuele Cazzola. On state classes and their dynamic semantics. In Joaquim Filipe, Boris Shishkov, and Markus Helfert, editors, Software and Data Technologies, volume 10 of Communications in Computer and Information Science, pages 84-96. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-70621-2_8 .

[16] Ferruccio Damiani, Elena Giachino, Paola Giannini, and Sophia Drossopoulou. A type safe state abstraction for coordination in Java-like languages. Acta Informatica, 45(7-8):479-536, 2008. http://dx.doi.org/10.1007/s00236-008-0079-y .

[17] Ferruccio Damiani, Paola Giannini, Alessandro Ricci, and Mirko Viroli. FEATHERWEIGHT AGENT LANGUAGE - A Core Calculus for Agents and Artifacts. In ICSOFT 2009 - Proceedings of the 4th International Conference on Software and Data Technologies, volume 1, pages 218-225. INSTICC Press, 2009.

[18] Ferruccio Damiani, Paola Giannini, Alessandro Ricci, and Mirko Viroli. A calculus of agents and artifacts. In Jose Cordeiro, AlpeshKumar Ranchordas, and Boris Shishkov, editors, Software and Data Technologies, volume 50 of Communications in Computer and Information Science, pages 124-136. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-20116-5_10 .

[19] Mehdi Dastani. 2APL: a Practical Agent Programming Language. Autonomous Agents and Multi-Agent Systems, 16(3):214-248, 2008. http://dx.doi.org/10.1007/s10458-008-9036-y .

[20] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. KLAIM: A Kernel Language for Agents Interaction and Mobility. IEEE Trans. Software Eng., 24(5):315-330, 1998. http://dx.doi.org/10.1109/32.685256 .

[21] Louise A. Dennis, Berndt Farwer, Rafael H. Bordini, Michael Fisher, and Michael Wooldridge. A common semantic basis for BDI languages. In Mehdi Dastani, Amal El Fallah Seghrouchni, Alessandro Ricci, and Michael Winiko, editors, Programming Multi-Agent Systems, volume 4908 of Lecture Notes in Computer Science, pages 124-139. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-79043-3_8 .

[22] Rogier M. van Eijk, Frank S. de Boer, Wiebe van der Hoek, and John-Jules Ch. Meyer. Operational semantics for agent communication languages. In Issues in Agent Communication, pages 80-95, London, UK, UK, 2000. Springer. http://dx.doi.org/10.1007/10722777_6 .

[23] Jacques Ferber and Olivier Gutknecht. Operational semantics of multi-agent organizations. In Intelligent Agents VI, Agent Theo- ries, Architectures, and Languages (ATAL), volume 1757 of Lecture Notes in Computer Science, pages 205-217. Springer, 2000. http://dx.doi.org/10.1007/10719619_15 .

[24] Cedric Fournet and Georges Gonthier. The Join Calculus: A Language for Distributed Mobile Programming. In Applied Semantics, Interna- tional Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, pages 268{332, London, UK, 2002. Springer. http://dx.doi.org/10.1007/3-540-45699-6_6 .

[25] Cedric Fournet, Georges Gonthier, Jean-Jacques Levy, Luc Maranget, and Didier Remy. A calculus of mobile agents. In Proceedings of the 7th International Conference on Concurrency Theory, CONCUR '96, pages 406-421, London, UK, 1996. Springer. http://dx.doi.org/10.1007/3-540-61604-7_67 .

[26] Philipp Haller and Martin Odersky. Actors that unify threads and events. In Proceedings of the 9th international conference on Coordination models and languages, COORDINATION'07, pages 171-190, Berlin, Heidelberg, 2007. Springer. http://dx.doi.org/10.1007/978-3-540-72794-1_10 .

[27] Matthew Hennessey and James Riely. Type-safe execution of mobile agents in anonymous networks. In Jan Vitek and Christian D. Jensen, editors, Secure Internet programming, pages 95-115. Springer, London, UK, UK, 1999. http://dx.doi.org/10.1007/3-540-48749-2_5 .

[28] Matthew Hennessy and James Riely. Resource access control in systems of mobile agents. Inf. Comput., 173(1):82-120, February 2002. http://dx.doi.org/10.1006/inco.2001.3089 .

[29] Koen Hindriks, Frank de Boer, Wiebe van der Hoek, and John-Jules Meyer. Formal semantics for an abstract agent programming language. In Munindar Singh, Anand Rao, and Michael Wooldridge, editors, Intelligent Agents IV Agent Theories, Architectures, and Languages, volume 1365 of Lecture Notes in Computer Science, pages 215-229. Springer, 1998. http://dx.doi.org/10.1007/BFb0026761 .

[30] Koen V. Hindriks. Programming rational agents in GOAL. In R. H. Bordini, M. Dastani, J. Dix, and A. El Fallah Seghrouchni, editors, Multi-Agent Programming: Languages, Platforms and Applications (2nd volume), pages 3-37. Springer, 2009.

[31] Kohei Honda and Mario Tokoro. An object calculus for asynchronous communication. In Pierre America, editor, ECOOP'91 European Conference on Object-Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 133-147. Springer, 1991. http://dx.doi.org/10.1007/BFb0057019 .

[32] Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems (ESOP), volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. http://dx.doi.org/10.1007/BFb0053567 .

[33] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming lan- guages, POPL '08, pages 273-284, New York, NY, USA, 2008. ACM. http://dx.doi.org/10.1145/1328438.1328472 .

[34] A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396-450, 2001. http://dx.doi.org/10.1145/503502.503505 .

[35] Atsushi Igarashi. A Featherweight Approach to FOOL. In Mira Mezini, editor, ECOOP 2011 - Object-Oriented Programming - 25th European Conference, Lancaster, UK, July 25-29, 2011 Proceedings, volume 6813 of Lecture Notes in Computer Science, page 433. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-22655-7 .

[36] G. S. Itzstein and D. Kearney. Join Java: an alternative concurrency semantics for Java. Technical Report ACRC-01-001, Univ. of South Australia, 2001.

[37] Nicholas R. Jennings. An agent-based approach for building complex software systems. Commun. ACM, 44(4):35-41, 2001. http://dx.doi.org/10.1145/367211.367250 .

[38] Christoph G. Jung and Klaus Fischer. A layered agent calculus with concurrent, continuous processes. In Proceedings of the 4th International Workshop on Intelligent Agents IV, Agent Theories, Architectures, and Languages, pages 245-258, London, UK, 1998. Springer. http://dx.doi.org/10.1007/BFb0026763 .

[39] Rajesh K. Karmani and Gul Agha. Actors. In Encyclopedia of Parallel Computing, pages 1-11. Springer, 2011.

[40] Rajesh Kumar Karmani, Amin Shali, and Gul Agha. Actor frameworks for the JVM platform: A Comparative Analysis. In In the proceedings of the 7th International Conference on the Principles and Practice of Programming in Java (PPPJ), pages 11-20, 2009. http://dx.doi.org/10.1145/1596655.1596658 .

[41] Naoki Kobayashi. Type systems for concurrent programs. In Bernhard Aichernig and Tom Maibaum, editors, Formal Methods at the Crossroads. From Panacea to Foundational Support, volume 2757 of Lecture Notes in Computer Science, pages 439-453. Springer, 2003. http://dx.doi.org/10.1007/978-3-540-40007-3_26 .

[42] Open System Laboratory. ActorFoundry, http://osl.cs.uiuc.edu/af/ .

[43] Y. Lesperance, H. J. Levesque, and R. Reiter. A situation calculus approach to modeling and programming agents. In Foundations of Rational Agency, pages 275-299. Kluwer, 1999.

[44] T. Massart. An agent calculus with simple actions where the enabling and disabling are derived operators. Information Processing Letters, 40(4):213 - 218, 1991. http://dx.doi.org/10.1016/0020-0190(91)90080-2 .

[45] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, i. Inf. Comput., 100(1):1-40, September 1992. http://dx.doi.org/10.1016/0890-5401(92)90008-4 .

[46] Alvaro F. Moreira, Renata Vieira, and Rafael H. Bordini. Extending the Operational Semantics of a BDI Agent-Oriented Programming Language for Introducing Speech-Act Based Communication. In Joao Leite, Andrea Omicini, Leon Sterling, and Paolo Torroni, editors, Declarative Agent Languages and Technologies, volume 2990 of Lecture Notes in Computer Science, pages 135-154. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-25932-9_8 .

[47] Andrea Omicini, Alessandro Ricci, and Mirko Viroli. Artifacts in the A&A Meta-Model for Multi-Agent Systems. Autonomous Agents and Multi-Agent Systems, 17, 2008. Special Issue on Foundations, Advanced Topics and Industrial Perspectives of Multi-Agent Systems. http://dx.doi.org/10.1007/s10458-008-9053-x .

[48] Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, 1996. http://dx.doi.org/10.1109/LICS.1993.287570 .

[49] A. S. Rao and M. P. George. BDI Agents: From Theory to Practice. In First International Conference on Multi Agent Systems (ICMAS95), 1995.

[50] Anand S. Rao. AgentSpeak(L): BDI agents speak out in a logical computable language. In Proceedings of the 7th European workshop on Modelling autonomous agents in a multi-agent world : agents breaking away: agents breaking away, MAAMAW '96, pages 42-55, Secaucus, NJ, USA, 1996. Springer.

[51] Alessandro Ricci and Andrea Santi. Typing Multi-Agent Programs in simpAL. In Proceedings of the Tenth International Workshop on Programming Multi-Agent Systems (ProMAS'12), pages 132-147, 2012.

[52] Alessandro Ricci, Mirko Viroli, and Maurizio Cimadamore. Prototyping Concurrent Systems with Agents and Artifacts: Framework and Core Calculus. Electron. Notes Theor. Comput. Sci., 194(4):111-132, 2008. http://dx.doi.org/10.1016/j.entcs.2008.03.102 .

[53] Alessandro Ricci, Mirko Viroli, and Giulio Piancastelli. simpA: An agent-oriented approach for programming concurrent applications on top of Java. Science of Computer Programming, 76(1):37 - 62, 2011. Selected papers from the 6th InternationalWorkshop on the Foundations of Coordination Languages and Software Architectures - FOCLASA'07. http://dx.doi.org/10.1016/j.scico.2010.06.012 .

[54] Stuart Russell and Peter Norvig. Articial Intelligence, A Modern Approach (second edition). Prentice Hall, 2003.

[55] Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. Location-independent communication for mobile agents: A two-level architecture. In ICCL Workshop: Internet Programming Languages, volume 1686 of Lecture Notes in Computer Science, pages 1-31. Springer, 1998. http://dx.doi.org/10.1007/3-540-47959-7_1 .

[56] Peter Sewell, Pawel T. Wojciechowski, and Asis Unyapoth. Nomadic pict: Programming languages, communication infrastructure overlays, and semantics for mobile computation. ACM Trans. Program. Lang. Syst., 32(4), 2010. http://dx.doi.org/10.1145/1734206.1734209 .

[57] Alexandru Suna and Amal El Fallah-Seghrouchni. Programming mobile intelligent agents: An operational semantics. Web Intelligence and Agent Systems, 5(1):47-67, 2007.

[58] Herb Sutter and James Larus. Software and the concurrency revolution. ACM Queue: Tomorrow's Computing Today, 3(7):54-62, September 2005. http://dx.doi.org/10.1145/1095408.1095421 .

[59] Danny Weyns, Andrea Omicini, and James J. Odell. Environment as a rst-class abstraction in multi-agent systems. Autonomous Agents and Multi-Agent Systems, 14(1):5-30, February 2007. Special Issue on Environments for Multi-agent Systems. http://dx.doi.org/10.1007/s10458-006-0012-0 .

[60] Michael Wooldridge and Nicholas R. Jennings. Intelligent agents: Theory and practice. Knowledge Engineering Review, 10:115-152, 1995. http://dx.doi.org/10.1017/S0269888900008122 .

[61] Mike Wooldridge. An Introduction to Multi-Agent Systems. John Wiley & Sons, Ltd, 2002.

[62] A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 1(115):38-94, 1994. http://dx.doi.org/10.1006/inco.1994.1093 .

[63] A Yonezawa and M Tokoro, editors. Object-oriented concurrent pro- gramming. MIT Press, Cambridge, MA, USA, 1986.

[64] Nobuko Yoshida and Matthew Hennessy. Assigning types to processes. Inf. Comput., 174(2):143-179, May 2002. http://dx.doi.org/10.1006/inco.2002.3113 .

On Safety Properties and Their Monitoring, pages 327-365

G. Roșu

Abstract | Full text | BibTeX | References | Article page

This paper addresses the problem of runtime verification from a foundational perspective, answering questions like ``Is there a consensus among the various definitions of a safety property?'' (Answer: Yes), ``How many safety properties exist?'' (Answer: As many as real numbers), ``How difficult is the problem of monitoring a safety property?'' (Answer: Arbitrarily complex), ``Is there any formalism that can express all safety properties?'' (Answer: No), etc. Various definitions of safety properties as sets of execution traces have been proposed in the literature, some over finite traces, others over infinite traces, yet others over both finite and infinite traces. By employing cardinality arguments and a novel notion of {em persistence}, this paper first establishes the existence of bijective correspondences between the various notions of safety property. It then shows that safety properties can be characterized as ``always past'' properties. Finally, it proposes a general notion of {em monitor}, which allows to show that safety properties correspond precisely to the monitorable properties, and then to establish that monitoring a safety property is arbitrarily hard.

Keywords: runtime verification, monitoring, safety properties

DOI: 10.7561/SACS.2012.2.327

[1] Martín Abadi and Leslie Lamport. The existence of renement mappings. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), pages 165-175. IEEE Computer Society, 1988. http://dx.doi.org/10.1109/LICS.1988.5115 .

[2] Martín Abadi and Leslie Lamport. The existence of renement mappings. Theoretical Computer Science, 82(2):253-284, 1991. http://dx.doi.org/10.1016/0304-3975(91)90224-P .

[3] Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Laurie Hendren, Sascha Kuzins, Ondrej Lhotak, Oege de Moor, Damien Sereni, Ganesh Sittampalam, and Julian Tibble. Adding trace matching with free variables to AspectJ. In Richard P. Gabriel, editor, ACM Conference on Object-Oriented Programming, Systems and Languages (OOPSLA), pages 345-364. ACM Press, 2005. http://dx.doi.org/10.1145/1094811.1094839 .

[4] Bowen Alpern and Fred B. Schneider. Dening liveness. Information Processing Letters, 21(4):181-185, 1985. http://dx.doi.org/10.1016/0020-0190(85)90056-0 .

[5] Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness in languages for distributed programming. In Fourteenth Annual ACM Symposium on Principles of Programming Languages (POPL' 87), pages 189-198, 1987. http://dx.doi.org/10.1145/41625.41642 .

[6] Feng Chen, Marcelo D'Amorim, and Grigore Rosu. Checking and correcting behaviors of Java programs at runtime with Java-MOP. In RV'05, volume 144(4) of Electronic Notes in Theoretical Computer Science. http://dx.doi.org/10.1016/j.entcs.2006.02.002 .

[7] Kevin W. Hamlen, J. Gregory Morrisett, and Fred B. Schneider. Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst., 28(1):175-205, 2006. http://dx.doi.org/10.1145/1111596.1111601 .

[8] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

[9] Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering., 3(2):125-143, 1977. http://dx.doi.org/10.1109/TSE.1977.229904 .

[10] Leslie Lamport. Logical foundation. In M. W. Alford, J. P. Ansart, G. Hommel, L. Lamport, B. Liskov, G. P. Mullery, F. B. Schneider, M. Paul, and H. J. Siegert, editors, Distributed systems: Methods and tools for specication. An advanced course, volume 190 of LNCS, pages 119-130. Springer-Verlag, 1985.

[11] Zohar Manna and Amir Pnueli. Temporal verication of reactive systems: safety. Springer-Verlag New York, Inc., New York, NY, USA, 1995.

[12] G. Rosu and M. Viswanathan. Testing extended regular language membership incrementally by rewriting. In RTA'03, volume 2706 of Lecture Notes in Computer Science, pages 499-514. Springer, 2003. http://dx.doi.org/10.1007/3-540-44881-0_35 .

[13] Fred B. Schneider. On Concurrent Programming. Springer, 1997.

[14] Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30-50, 2000. http://dx.doi.org/10.1145/353323.353382 .

Position Automata for Kleene Algebra with Tests, pages 367-394

A. Silva

Abstract | Full text | BibTeX | References | Article page

Kleene algebra with tests (KAT) is an equational system that combines Kleene and Boolean algebras. One can model basic programming constructs and assertions in KAT, which allowed for its application in compiler optimization, program transformation and dataflow analysis. To provide semantics for KAT expressions, Kozen first introduced emph{automata on guarded strings}, showing that the regular sets of guarded strings plays the same role in KAT as regular languages play in Kleene algebra. Recently, Kozen described an elegant algorithm, based on ``derivatives'', to construct a deterministic automaton that accepts the guarded strings denoted by a KAT expression. This algorithm generalizes Brzozowski's algorithm for regular expressions and inherits its inefficiency arising from the explicit computation of derivatives. In the context of classical regular expressions, many efficient algorithms to compile expressions to automata have been proposed. One of those algorithms was devised by Berry and Sethi in the 80's (we shall refer to it as Berry-Sethi construction/algorithm, but in the literature it is also referred to as position or Glushkov automata algorithm). In this paper, we show how the Berry-Sethi algorithm can be used to compile a $KAT$ expression to an automaton on guarded strings. Moreover, we propose a new automata model for KAT expressions and adapt the construction of Berry and Sethi to this new model.

Keywords: position automata, Kleene algebra with tests, coalgebra

DOI: 10.7561/SACS.2012.2.367

[1] Allegra Angus and Dexter Kozen. Kleene algebra with tests and pro- gram schematology. Technical Report TR2001-1844, Computing and Information Science, Cornell University, July 2001.

[2] Valentin M. Antimirov. Partial derivatives of regular expressions and nite automaton constructions. Theor. Comput. Sci., 155(2):291-319, 1996. http://dx.doi.org/10.1016/0304-3975(95)00182-4 .

[3] Falk Bartels. On generalized coinduction and probabilistic specication formats. PhD thesis, Vrije Universiteit Amsterdam, 2004. PhD thesis.

[4] Gerard Berry and Ravi Sethi. From regular expressions to deterministic automata. Theor. Comput. Sci., 48(3):117-126, 1986. http://dx.doi.org/10.1016/0304-3975(86)90088-5 .

[5] Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481-494, 1964. http://dx.doi.org/10.1145/321239.321249 .

[6] Jean-Marc Champarnaud, Florent Nicart, and Djelloul Ziadi. From the ZPC structure of a regular expression to its follow automaton. IJAC, 16(1):17-34, 2006. http://dx.doi.org/10.1142/S0218196706002895 .

[7] Jean-Marc Champarnaud and Djelloul Ziadi. Canonical derivatives, partial derivatives and nite automaton constructions. Theor. Comput. Sci., 289(1):137-163, 2002. http://dx.doi.org/10.1016/S0304-3975(01)00267-5 .

[8] V.M. Glushkov. The abstract theory of automata. Russian Math. Surveys, 16:1-53, 1961. http://dx.doi.org/10.1070/RM1961v016n05ABEH004112 .

[9] Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and Jose Meseguer, editors, Essays Dedicated to Joseph A. Goguen, volume 4060 of Lecture Notes in Computer Science, pages 375-404. Springer, 2006. http://dx.doi.org/10.1007/11780274_20 .

[10] Donald M. Kaplan. Regular expressions and the equivalence of pro- grams. J. Comput. Syst. Sci., 3(4):361-386, 1969. http://dx.doi.org/10.1016/S0022-0000(69)80027-9 .

[11] Dexter Kozen. Automata and Computability. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1997.

[12] Dexter Kozen. Automata on guarded strings and applications. Matematica Contempor^anea, 24:117-139, 2003.

[13] Dexter Kozen. Nonlocal ow of control and Kleene algebra with tests. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 105-117. IEEE Computer Society, 2008. http://dx.doi.org/10.1109/LICS.2008.32 .

[14] Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. Technical Report http://hdl.handle.net/1813/10173 , Computing and Information Science, Cornell University, March 2008.

[15] Dexter Kozen and Maria-Christina Patron. Certication of com- piler optimizations using Kleene algebra with tests. In John W. Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Lus Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Computational Logic, volume 1861 of Lecture Notes in Computer Science, pages 568-582. Springer, 2000. http://dx.doi.org/10.1007/3-540-44957-4_38 .

[16] Robert McNaughton and H. Yamada. Regular expressions and state graphs for automata. IRE Transactions on Electronic Computers, 9(1):39-47, 1960. http://dx.doi.org/10.1109/TEC.1960.5221603 .

[17] Michael O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:114-125, 1959. http://dx.doi.org/10.1147/rd.32.0114 .

[18] Jan J. M. M. Rutten. Automata and coinduction (an exercise in coalge- bra). In Davide Sangiorgi and Robert de Simone, editors, CONCUR, volume 1466 of Lecture Notes in Computer Science, pages 194-218. Springer, 1998. http://dx.doi.org/10.1007/BFb0055624 .

[19] Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. http://dx.doi.org/10.1016/S0304-3975(00)00056-6 .

[20] Alexandra Silva. Kleene coalgebra. PhD thesis, Radboud University Nijmegen, 2010.

[21] Ken Thompson. Programming techniques: Regular expression search algorithm. Commun. ACM, 11(6):419-422, 1968. http://dx.doi.org/10.1145/363347.363387 .

Faculty of
Computer Science

Scientific Annals of Computer Science

"Alexandru Ioan Cuza" University of Iaşi

Volume XXII, Issue 2, 2012

Faculty ofComputer Science

Scientific Annals of Computer Science

"Alexandru Ioan Cuza" University of Iaşi

Volume XXII, Issue 2, 2012

Faculty of
Computer Science