Qais

Quantitative analysis of interacting systems: foundations and algorithms

Quantitative analysis of interacting systems: foundations and algorithms

Summary [5000]

In recent years, there has been an increasing interest in studying the behavior of software systems from a quantitative perspective. Such an interest is actually driven by concrete challenges coming from the engineering practice. It is widely recognized that to suitably meet these challenges requires the development of both solid foundations and derived techniques. Such is the starting point of this project.

As an illustration, consider a service-based application running in a call center performing matching between customers and operators. Typical questions about such system include:

(1) How far is the system with "n" operators from an ideal system where the customer never waits (and the number of free operators is not too high)?

(2) For which values of "n", along the course of the day, are the behaviors of the current system and ideal system closer?

(3) How can customer feedback about the match between the requested service and the offered be used to improve following calls?

Their relevance cannot be understated: the resources needed to keep a system running, such as the number of operators or memory available in a computer, are not infinite and it is of the utmost importance to decrease the use of resources and at the same time keep a reasonable performance. To properly answer this sort of questions, however, entails the need for techniques aimed at analyzing systems from a quantitative perspective, as well as for robust algorithms which implement them.

In broad terms, the analysis of the behaviour of computing devices is an evergreen subject of computer science. Defining “what is the behaviour of a system” or “when two systems behave the same” is a fundamental issue from its dawn till nowadays. Many different (behavioural) equivalences have been introduced for different kinds of systems (e.g., functional, non-deterministic and concurrent systems) and a huge “corpus of conceptual and computational tools” consisting of algorithms, proof’s techniques, rules formats and different sorts of languages has been developed to reason about systems and their behavioural equivalences.

What has recently emerged from the software industrial practice (namely in safety-critical domains and hybrid design) is the need to take into account explicitly, when reasoning about systems' behaviour, quantitative properties, for which existing equivalences are somehow inadequate, since they only allow “boolean reasoning”: either two systems are equivalent or they are not.

Motivated by these considerations, several notions of behavioural metrics or closely related approaches have been proposed. Differently from the ordinary equivalences, behavioural metrics express the distance between the behaviours of systems. A major challenge in this context concerns the fact that many of the conceptual and computational tools mentioned above being not yet available for metrics.

This projects adopts a new approach: it proposes to “lift” such tools from equivalences to metrics by employing the theory of coalgebras. Note that many important tools developed for equivalences are concrete instances of abstract coalgebraic results. On the other hand, the genericity of coalgebraic constructions, which are parametric on the model of the underlying behaviour structure, offers a general setting to frame different sorts of behavioural reasoning, including quantitative modelling, analysis and metrics. Applications of coalgebra theory to probabilistic transition systems lead to the design of one of the most efficient, known algorithms for computing metrics (see [vBW]) which is an encouraging result for our own research programme.

The envisaged contributions are placed at three different levels. First, from a foundational perspective, we propose to advance the state of the art in the theory of metric behavioural equivalences. Secondly, we intend to make the theory operational by developing efficient algorithms to compute the distance between two systems. Such algorithms will be rendered as plug-ins to the core of a prototype tool and its effectiveness tested in an exisiting service-oriented software system. As a third contribution, on the applications side, we intend to add the quantitative dimension (theory and techniques) to Reo, a component based specification language, and use such an enriched framework to analyze and transform service-oriented systems.

A main case-study will be supplied by the dutch company Almende: the ASK system, an industrial software system for connecting service providers and consumers (for instance, the call center example above is one of its instantitations). ASK has been modeled in Reo, which will make possible to use and extend its original model in order to obtain a detailed analysis of the quantitative properties of the system. The outcome of such analysis will help both the developers and the installations of the ASK system to tune resource allocation in order to improve the performance of the system.

Sumário [5000]

O interesse pelo estudo rigoroso do comportamento dos sistemas a partir de um ponto de vista quantitativo tem vindo a crescer quer no campo académico quer na indústria. De facto, tal interesse é motivado por desafios complexos na prática da Engenharia dos sistemas informáticos. É hoje consensual que uma resposta adequada a esses desafios requer o desenvolvimento tanto de fundamentos matemáticos sólidos como das técnicas de análise e verificação deles derivadas. Tal é objectivo deste projecto.

Como ilustração, considere-se uma aplicação baseada em serviços instalada num call center para estabelecimento e manutenção de ligações entre clientes e operadores. Típicas questões neste domínio serão

(1) Qual a distância entre o sistema típico com n utilizadores e um sistema ideal em que o cliente nunca espera (e o número de operadores é livre, embora não excessivo)?

(2) Para que valores de n, ao longo do dia, é que os comportamentos do sistema real e do ideal se aproximam?

(3) De que modo o feedback manifestado por cliente sobre o serviço requerido e o oferecido, é usado para melhoria do nível do serviço?

A relevância destas questões não pode ser iludida: os recursos necessários para manter um sistema activo, tais como o número de operadores e a memória disponível, não são infinitos. É, neste contexto, da maior importância decrementar o uso de recursos e, ao mesmo tempo, manter um nível de desempenho adequado. Para responder as estas questões, contudo, torna-se necessário desenvolver técnicas para análise quantitativa dos sistemas e algoritmos robustos que as implementem.

Em termos gerias, a análise do comportamento dos sistemas computacionais constitui um tópico quente e recorrente de investigação. A definição daquilo que é o comportamento de um sistema ou a indagação sobre se dois sistemas se comportam de forma análoga, é já uma preocupação antiga. Muitas equivalência (comportamentais) foram introduzidas para diferentes tipos de sistemas (e.g., funcionais, não determinísticos ou concorrentes) e um enorme corpus conceptual e de ferramentas, incluindo algoritmos, técnicas de prova, formatos de regras e linguagens, desenvolvido para raciocinar sobre sistemas complexos e suas equivalências comportamentais.

O que emergiu mais recentemente da pratica industrial (nomeadamente em software critico e em sistemas hídricos) foi a necessidade de tomar em consideração de forma explícita, ao raciocinar sobre comportamento, propriedades de natureza quantitativa para as quais as equivalência estudadas na literatura são insuficientes. Estas limitam-se, regra geral, a conclusões booleanas: ou os sistemas são ou não são equivalentes.

Motivadas por este tipo de considerações, diferentes noções de métricas comportamentais, e outras aproximações similares, têm sido propostas. Ao contrário das equivalências comportamentais clássicas, estas métricas quantificam a distância entre comportamentos. No entanto, a maioria das ferramentas computacionais e conceptuais disponíveis não estão equipadas com suporte adequado para este tipo de métricas.

Este projecto adopta uma nova aproximação: propõem-se estender tais ferramentas a métricas, recorrendo à teoria das coalgebras. Note-se que a maior parte das ferramentas orientadas às equivalências clássicas são, de facto, concretizações de resultados abstractos em coalgebras. Por outro lado, a generalidade das construções coalgébrias, paramétrica no modelo escolhido para captar o comportamento subjacente, oferece um contexto formal para enquadrar diferentes tipos de raciocínio comportamental, incluindo modelação quantitativa, análise e métricas. Aplicações da teoria das coalgebras a sistemas de transição probabilísticos levou à concepção de um dos algoritmos mais eficientes para cálculos de métricas (ver [vBW]), o que é um resultado encorajador para o nosso próprio programa de investigação.

O projecto visa contribuir a três níveis distintos. Primeiro, numa perspectiva fundamental, propõe-se fazer avançar o estado da arte na teoria das equivalência com base em métricas comportamentais. Em segundo lugar pretende-se operacionalizar essa teoria através do desenvolvimento de algoritmos eficientes para calcular a distância comportamental entre dois sistemas. Tais algoritmos serão disponibilizados como plug-ins de uma ferramenta de prototipagem e a sua adequação técnica testada com dados (sistemas) reais.

Finalmente, ao nível das aplicações, o projecto propõe-se incorporar a dimensão quantitativa (teorias e técnicas) em Reo e utilizar esta plataforma para analisar e transformar sistemas baseados em serviços.

Uma estudo de caso de dimensão não trivial será fornecido pela empresa holandesa Almende: o sistema ASK. Trata-se de um pacote comercial para interligar fornecedores e clientes de serviços. ASK foi já modelado em Reo, o que torna possível usar e estender esse modelo original para obter uma análise detalhada das propriedades de natureza quantitativa do sistema. Os resultados dessa análise apoiarão quer os que desenvolvem este sistema quer os que o instalam e mantém, no apuramento e controlo da alocação de recursos de forma a melhorar o seu desempenho.

Literature Review [6000]

* Coalgebraic metric bisimulations (relevant for tasks T1, T2 and T3)

Desharnais, Gupta, Jagadeesan and Panangaden [DGJP] proposed a notion of behavioural (pseudo)metric for probabilistic transition systems. Later, van Breugel and Worrel took a more coalgebraic view on the work of [DGJP], providing the connection with linear programming and constructing the final coalgebra in the category of metric spaces and contractive maps. The metric in both papers is defined in the style of Milner-Park’s bisimilarity: it is the greatest fixpoint of a monotone function over the (partially ordered) set of metrics. The work in [vBW] introduces the most efficient algorithm for computing metrics up to date. It is done for a particular type of quantitative system and the results are based on coalgebras. We see this as a witness that the use of coalgebras to achieve the aims of this project is promising.

* Stochastic Reo (relevant for task T4)

Reo [Arb] is a channel-based coordination model wherein so-called connectors are used to coordinate (i.e., control the communication among) com- ponents or services exogenously (from outside of those components and services). In Reo, complex connectors are compositionally built out of primitive channels. Stochastic Reo [MSKA] is an extension of Reo where channel ends and channels are annotated with stochastic values for data arrival rates at channel ends and processing delay rates on channels. Such rates are, e.g., non-negative real values that describe how the probability that an event occurs varies with time. As a specification language Reo is intuitive and it has been applied to real systems, including the one mentioned in T4. However, the focus on the research on Reo and its variants has been on modelling and expressiveness and no work on equivalence reasoning has been done so far. We believe that the results of this project will add value to the theory and tools available for Reo.

* QoS? of distributed systems(relevant for T4 and T5)

The project identifies a specific application area: the development of a calculus of QoS? -robust composition of software services, resorting to the concepts and techniques delivered by the Tasks T1 to T3. With the growing complexity and size of modern distributed systems, the need for models to support their architectures, design their coordination, and manage their QoS? at run time has become a critical issue. To build large-scale distributed applications, one often needs to select components/services from a set of functionally equivalent candidates, meaning, those that implement the same functionality but differ in their non-functional characteristics, i.e., QoS? properties. Therefore, a important aspect of service composition relates to the management of the QoS? requirements, a topic clearly in the scope of application of the present proposal.

QoS? of distributed systems refers to a wide range of quality metrics, including, for example, availability, reliability, security, flexibility, performance (response time, for instance), and so on (see e.g. [LBNDKC]). Over the past few decades, several quantitative stochastic methods (e.g., stochastic Petri Nets, interactive Markov Chains) have been proposed and used in a variety of application areas to study different QoS? metrics. Different kinds of extensions of process algebras have been developed for performance evaluation, including timed process algebras, probabilistic process algebras, and stochastic process algebras. These process algebra-based approaches are compositional at a fine-grain level, which makes them difficult to use them for composing services in an architecturally meaningful way as black boxes. Coordination based models, such a Reo, in which both application in T5 and case study in T4 will be framed, provides a more structural approach to interaction control. In general, however, and to a large extent, existing formal models for service composition lack sound, pragmatic means for reasoning about QoS? properties.

It is expected this project contributes to further extending current models and techniques to make them suitable for architecture-based assessment and monitoring of the end-to-end QoS? of large-scale service-oriented applications. Specifically, the project aims at defining a QoS? -aware architectural model on top of Reo and a notion of robust service composition. Preliminary results obtained within the project team are reported in [MB]. QoS? -robustness is intended to measure the quality of response to unpredictable change and avoidance of failure. Robustness is studied in several contexts. Relevant to the approach this project aims at exploring is research on game-theoretic semantics. Game-theoretic approaches [Abr] enable a fine-grained understanding of the logical principles underlying interaction based on the system’s structure, which may provide an interesting alternative to model endurance to failure.

* The team's research.

The team has extensive research in coalgebraic methods in computer science [BRS,Mon,Mon98,BM09] and quantitative models, which frames the research proposal in tasks T1, T2 and T3. From the applicational side, with relevance to tasks T4 and T5, the team is also recognized for contributions in models and calculi for component-based and service-oriented software [RB,BB] and QoS analysis [BBRS,MB,MSKA,SBRS].

Plan and Methods [10000]

Reasoning about the behavior of software systems is a topic that has occupied computer scientists since the beggining of the field. For many years, the formal methods community has focussed on critical software systems, such the ones running on an airplane or space shuttle, and techniques such as model-checking are by now well-established and effective in assessing the validity of crutial properties. In the last few years, attempts on tranferring these techniques too mainstream software systems have been made, but they were shown innaproppriate: for most systems, one does not want a property to hold, but instead one wants to assess that a certain property holds in 99% of the cases. Think of the call center example in the summary: the company does not strictly want that clients never wait more than 1 minute, but instead they want to ensure, for instance, that in 90% of the cases this happens.

This type of ``quantitative reasoning'' is now gaining popularity and in the next few years it will be one of the most relevant topics in Computer Science research.

Our proposal fits in this line of research and we are aware that any relevant contribution

  • requires solid foundational work
  • as well as relevant empirical work, with concrete case studies and tools illustratting the effectiveness of the approach

Therefore, this proposal contains:

(1) Two foundational tasks, contributing to the state of the art in reasoning about the equivalence of quantitative models.

(2) One operational task, in which efficient algorithms to compute the equivalences derived in (1) will be devised.

(3) One case study, where we intend to transfer the techniques developed to a real software system. This empirical work will be developed jointly with the dutch company Almende.

(4) One application-oriented task, in which theoretical results, techniques and tools developed in the project are integrated to address a relevant and difficult problem in service-oriented design: the characterization QoS-robustness for services and an associated calculus of QoS-robust composition.

In the sequel, we explain the essence of our approach and the potential of the research team.

Vision

Both from a theoretical and a technological point of view, global computing raises a number of challenging and difficult research questions whose relevance for the future of Software Engineering cannot be underestimated. On the theory side, examples include the quest for interaction models, coordination calculi, foundations for co-operation and mobility, resource usage and security, semantics and methods for service specification, orchestration and deployment, among many others.

On the other hand, long term research in coalgebra theory and coindution provided an useful set of both conceptual and methodological tools to study the the semantics of reactive, interactive and mutable systems.

The envisaged approach in this project touchs upon several sides of the research spectrum: foundational, applicational and experimental.

At a foundational level, the project will introduce new notions of equivalence, more appropriate to reason about quantitative properties of models of computation. In short, at this level, our approach will be coalgebraic. The strength of the coalgebraic approach lies in the fact that notions are developed uniformly parametrized on the type of the system, which enables the development of notions and tools for a large class of models at the same time.

At the applicational level, we will devise efficient algorithms to compute the equivalences developed in the previous point and develop prototype tools, to be made available publicly.

At the experimental level, the project aims at applying all the techniques developed at the other two levels to a real case study. This will validate the general framework and show its generality does not constrain its application.

In short, this proposal combines foundational research with engineering work, the latter supported by a Dutch software company, Almende. It fosters the cooperation between two national groups at the University of Minho and University of Lisbon, who already share interest in coalgebraic semantics, but have complementary skills. The groups have jointly organized a series of Joint Research Workshops on ``Coinduction, Interaction and Composition'', which brought together research groups on both coalgebraic methods and their application to the development of models and calculi for interaction, composition and coordination of software components and services.

The team

This research program builds upon the team's extensive research on

  • coalgebraic methods in computer science [BRS,Mon,Mon98,BM09],
  • analysis of quantitative models and QoS? -aware formal methods [BBRS,MB,MSKA,SBRS,MO].

The foundational results and techniques to be developed in Tasks T1, T2 and T3, will be applied to a hot research topic in the semantics of service-orientation (T5) and to a related case study (T4). Again this is rooted on the team's previous work on

  • models and calculi for software interconnection and architectures [BB,RB,BCS,BCS11]

Dynamic reconfigurable service architectures is precisely the topic of another FCT-funded project (Mondrian - PTDC/EIA-CCO/108302/2008), coordinated by a member of this team. Actually, one of the motivations for this proposal came from current research in Mondrian: crescent awareness of the role of QoS? measures to drive software reconfiguration and, correspondingly, the need for effective techniques and algorithms for formal quantitative analysis.

The team previous work will be further strengthened by the involvement of Prof.dr. F. Arbab (CWI), the inventor of Reo, and with whom we have on-going collaboration, Prof.dr. P. Panangaden (McGill), an expert on Markov processes, and Prof.dr. C. Baier, an expert on probabilistic model-checking. Previous work, namely in the context of European projects, with the proposed consultants, bears sustainability to the envisaged collaboration.

The elements of the team have supervised a number of PhD? projects in related areas, posses an interesting publication record and maintain close collaborations with leading research international groups (eg the Foundations of Software Engineering cluster at CWI, Amsterdam, the group of Dexter Kozen, at Cornell University and the Comete group, headed by C. Palamidessi, at INRIA).

Two additional aspects should be mentioned about the team. First, by combining synergies of the two portuguese research groups on coalgebra theory and applications (in Minho and Lisbon), the project has the potential to establish of a new, pioneering area of expertise for both groups at University of Minho and New University of Lisbon. It is, thus, a starting point for the near future, but rooted, as mentioned above, in a previous series of joint seminars and workshops organized every year since 2006.

A second aspect concerns the team choice for PI: a recent, post-doc fellow at UM, with a remarkable record of publications in the project's target area, will serve as project coordinator. QUAIS is expected to frame her post-doc training in a broader context and to boost a new, exciting research area (that of coalgebraic foundations and techniques for quantitative analysis of interactive systems) on top of a well-established domain (that of coalgebraic methods) in which both the PI and Minho-Lisbon teams have relevant contributions. This corresponds to our vision of on the role of a post-doc fellow in the national scientific network.

Tasks

Timeline and Management

Most management effort will be dedicated to ensure that tasks proceed according to the established plan, and that milestones are delivered on time. Special care will be taken with critical milestones, on which other tasks depend. Such is the case of milestone ...

The following activities are planed in order to ensure coordination between team members:

- A bi-monthly seminar, alternating between UM and UNL, will be held with all members active in the project at the time;

- Each of these meetings will be complemented with a technical presentation by one of the project members; these talks will be open to the research community and each project member is required to give at least one such talk;

-A research workshop will be held every year, in September, to assess the project progress and provide a forum, open to the scientific community to present and validate work-in-progress.

- A collaborative site will be launched at the start of the project; besides serving as the main diffusion point of the project, it will include a private area to share documents and scribble current research ideas.

The team considers extremely relevant to the success of this project and to the international dissemination of its results, the role of consultants (see below justifications and tasks assigned).

To maximize the revenue from the project budget, the following measures will be taken:

- Submissions to conferences will follow according to a plan defined by the PI, in order to avoid spending the mission budget in events which are not relevant to the project; this plan will mainly include first tier international conferences mentioned in the individual task descriptions.

- To fully benefit from consultants expertise, each visit will start with a one-day informal workshop where all active team members are expected to give a short talk; by these we expect the consultant to get acquainted with the overall project status, thus increasing the potential for effective and relevant scientific discussions;

- Apart from the usual meetings with their designated supervisors, all BI grant holders will be requested to submit every 3 months a progress report to ensure that the research plan is progressing as expected.

One senior management official will be designated by each partner (UM and UNL) to help with financial planning, and progress/final reports to FCT.

Some ideas for milestones:

  1. M1: Coalgebraic metrics (preliminary results on tasks T1 and T2; workshop with consultants C. Baier and P. Panangaden)

  1. M2: Prototype tool (Prototype tool (T3))

  1. M3: Calculus of QoS? -robust service composition (Modelling language plus simulator (T5))

  1. M4: Case study (Experimental report on the analysis of the ASK system (T4); workshop with consultants F. Arbab and C.Baier)

Past Publications [5]

[BBRS] Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, Alexandra Silva: Deriving Syntax and Axioms for Quantitative Regular Behaviours. CONCUR 2009: 146-162, Springer

[Mon] Luís Monteiro: A Coalgebraic Characterization of Behaviours in the Linear Time - Branching Time Spectrum. WADT 2008: 251-265

[MSKA] Young-Joo Moon, Alexandra Silva, Christian Krause, Farhad Arbab: A Compositional Model to Reason about end-to-end QoS in Stochastic Reo Connectors. Science of Computer Programming. 2011. Accepted for publication.

[RB] Nuno F. Rodrigues, Luís Soares Barbosa: Slicing for architectural analysis. Science of Computer Programming 75(10): 828-847 (2010)

[SBBR] Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten: Quantitative Kleene Coalgebras. Information and Computation. 2011. In Press.

Bibliographic References [30]

[Abr] S. Abramsky. Algorithmic game semantics: A tutorial introduction. In H. Schichtenberg and R. Steinbruggen, editors, Proceedings of the NATO Advanced Study Institute, Marktoberdorf, pages 21–47. Kluwer Academic Publishers, 2001

[Arb] F. Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science (MSCS) 14(3):329-366 (2004)

[ABBR] F. Alessi, P. Baldan, G. Bellè, and J. J. M. M. Rutten. Solutions of functorial and nonfunctorial metric domain equations. Electr. Notes Theor. Comput. Sci., 1, 1995

[BB] Marco Barbosa, Luís Soares Barbosa: A perspective on service orchestration. Science of Computer Programming 74(9): 671-687 (2009)

[BM09] Luís Soares Barbosa and Sun Meng: A coalgebraic semantic framework for reasoning about interaction designs in UML2 Semantics and Applications, Kevin Lano (ed), John Wiley and Sons, Inc., pp 249-279 (2009)

[BSdV] Falk Bartels, Ana Sokolova, Erik P. de Vink: A hierarchy of probabilistic system types. Theor. Comput. Sci. 327(1-2): 3-22 (2004)

[BM] F. Bonchi and U. Montanari. Minimization algorithm for symbolic bisimilarity. In ESOP, volume 5502 of LNCS, pages 267–284. Springer, 2009.

[BvBR] M. M. Bonsangue, F. van Breugel, and J. J. M. M. Rutten. Generalized metric spaces: Completion, topology, and powerdomains via the Yoneda embedding. Theoretical Computer Science, 193(1-2):1–51, 1998.

[BCS] M. M. Bonsangue, D. Clarke and A. Silva. Automata for Context-dependent Connectors.Accepted for Coordination 2009. In J. Field and V. Vasconcelos, editors, proceedings COORDINATION 2009, LNCS 5521, Springer, 2009, pp. 184--203.

[BCS11] M. M. Bonsangue, D. Clarke and A. Silva. A model of context-dependent component connectors. Science of Computer Programming. In press.

[BRS] M. M. Bonsangue, Jan J. M. M. Rutten, Alexandra Silva: An Algebra for Kripke Polynomial Coalgebras. LICS 2009: 49-58

[vBW] F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331(1):115–142, 2005

[DGJP] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled markov processes. Theoretical Computer Science, 318a(3):323–354, 2004.

[DJGP] J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Logic in Computer Science, pages 413–422. IEEE, 2002.

[FM] J.-C. Fernandez and L. Mounier. “on the fly“ verification of behavioural equivalences and preorders. In CAV, volume 575 of LNCS, pages 18a1–191. Springer, 1992.

[Her] U. Herzog: Formal Description, Time and Performance Analysis. A Framework. Entwurf und Betrieb verteilter Systeme 1990: 172-190

[Hir] D. Hirschkoff. On the benefits of using the up-to techniques for bisimulation verification. In TACAS, volume 1579 of LNCS, pages 285–299. Springer, 1999.

[LBNDKC] Liangzhao Zeng, Boualem Benatallah, Anne H.H. Ngu, Marlon Dumas, Jayant Kalagnanam, and Henry Chang. QoS? -Aware Middleware for Web Services Composition. IEEE Transactions on Software Engineering, 30(5):311–327, 2004

[LS] K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, 1991.

[JY] B. Jonsson and W. Yi. Compositional testing preorders for probabilistic processes. In LICS, pages 431–441. IEEE, 1995.

[MO] H. Macedo, José Nuno Oliveira. Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra. In MPC, volume 6120 of LNCS, pages 271–287. Springer, 2010.

[Mon98] Luís Monteiro: Semantic domains based on sets with families of equivalences. Electr. Notes Theor. Comput. Sci. 11: (1998)

[MB] Sun Meng, Luís Soares Barbosa: Towards the introduction of QoS information in a component model. In 2010 ACM SAC, pages 2045–2046. ACM, 2010.

[PHW] A. D. Pierro, C. Hankin, and H. Wiklicky. Quantitative relations and approximate process equivalences. In CONCUR, volume 2761 of LNCS, pages 271–287. Springer, 2003.

[Rut98] J. J. M. M. Rutten. Relators and metric bisimulations. Electr. Notes Theor. Comput. Sci., 11, 1998.

[Rut00] J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, 2000.

[Rut07] J. J. M. M. Rutten. Coalgebraic foundations of linear systems. In CALCO, volume 4624 of LNCS, pages 425–446. Springer, 2007.

[SL] R. Segala and N. A. Lynch. Probabilistic simulations for probabilistic processes. In CONCUR, volume 836 of LNCS, pages 481–496. Springer, 1994.

[TR] D. Turi and J. J. M. M. Rutten. On the foundations of final coalgebra semantics. Mathematical Structures in Computer Science, 8(5):481–540, 1998.

[Wor] J. Worrell. Coinduction for recursive data types: partial orders, metric spaces and omega-categories. Electr. Notes Theor. Comput. Sci., 33, 2000.

r17 - 06 Jan 2012 - 16:19:20 - AlexandraSilva
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM