Skip to main content
SpringerLink
Log in

Decomposing Global Quantitative Properties into Local Ones

  • Conference paper
  • First Online:
Data Privacy Management and Security Assurance (DPM 2016, QASA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 9963))

  • 706 Accesses

Abstract

In this paper we address the problem of identifying what local properties the sub-components of a system have to satisfy in order to guarantee a (security) property on the behaviour of the whole system. We associate each action with a value. Hence, we end up with quantitative properties on them, which are specified through a modal logic equipped with a parametric algebraic structure (i.e., a c-semiring). The aim is to have a value related to the satisfaction of a formula. Starting from the behaviour of a general distributed system (or context), we propose a formal approach to decompose a global quantitative property into the local quantitative properties to be satisfied by its sub-contexts.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Boolean c-semirings can be used to model crisp problems.

  2. 2.

    \(\mathbb K\) is complete if it is closed with respect to infinite sums, and the distributivity law holds also for an infinite number of summands [2].

  3. 3.

    It is worth noting that this follows the notion of weakly validity introduced in [11].

  4. 4.

    At this level, we are not interested in values \(t,t_{1},t_{2}\) and so on, hence we do not calculate their exact value as the product of \(k_{a}\) and \(k_{b}\).

References

  1. Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: 2nd International Workshop on Hybrid Systems and Biology, EPTCS, vol. 125, pp. 3–19 (2013)

    Google Scholar 

  2. Bistarelli, S., Gadducci, F.: Enhancing constraints manipulation in semiring-based formalisms. In: ECAI, pp. 63–67 (2006)

    Google Scholar 

  3. Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. J. ACM 44(2), 201–236 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bistarelli, S., Santini, F.: Two trust networks in one: using bipolar structures to fuse trust and distrust. In: 2014 Twelfth Annual International Conference on Privacy, Security and Trust, pp. 383–390. IEEE (2014)

    Google Scholar 

  5. Bistarelli, S., Santini, F., Martinelli, F., Matteucci, I.: Automated adaptation via quantitative partial model checking. In: Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1993–1996. ACM (2016)

    Google Scholar 

  6. Blyth, T.S., Janowitz, M.F.: Residuation Theory, vol. 102. Pergamon press, Oxford (1972)

    MATH  Google Scholar 

  7. Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. ENTCS 220(3), 61–77 (2008)

    MATH  Google Scholar 

  8. Gardelli, L., Viroli, M., Omicini, A.: Design patterns for self-organising systems. In: Burkhard, H.-D., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds.) CEEMAS 2007. LNCS, vol. 4696, pp. 123–132. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Golan, J.: Semirings and Affine Equations Over Them: Theory and Applications. Kluwer Academic Pub., Dordrecht (2003)

    Book  MATH  Google Scholar 

  10. Juhl, L., Larsen, K.G., Srba, J.: Modal transition systems with weight intervals. J. Log. Algebr. Program. 81(4), 408–421 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  11. Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. J. Logic Comput. 1(6), 761–795 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  12. Li, J., Yarvis, M., Reiher, P.: Securing distributed adaptation. Comput. Netw. 38(3), 347–371 (2002)

    Article  Google Scholar 

  13. Lluch-Lafuente, A., Montanari, U.: Quantitative mu-calculus and CTL defined over constraint semirings. TCS 346(1), 135–160 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  14. Martín, J.A., Martinelli, F., Pimentel, E.: Synthesis of secure adaptors. J. Log. Algebr. Program. 81(2), 99–126 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  15. Martinelli, F., Matteucci, I., Santini, F.: Semiring-based specification approaches for quantitative security. In: Proceedings Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL, EPTCS, vol. 194, pp. 95–109 (2015)

    Google Scholar 

  16. Martinelli, F., Matteucci, I., Santini, F.: There are two sides to every question. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 304–318. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25527-9_20

    Chapter  Google Scholar 

  17. Splunter, S., Wijngaards, N.J.E., Brazier, F.M.T.: Structuring agents for adaptation. In: Alonso, E., Kudenko, D., Kazakov, D. (eds.) AAMAS 2001-2002. LNCS, vol. 2636, pp. 174–186. Springer, Heidelberg (2003). doi:10.1007/3-540-44826-8_11

    Chapter  Google Scholar 

  18. Viganò, L.: Automated security protocol analysis with the AVISPA tool. ENTCS 155, 69–86 (2006)

    Google Scholar 

  19. De Wolf, T., Holvoet, T.: Design patterns for decentralised coordination in self-organising emergent systems. In: Brueckner, S.A., Hassas, S., Jelasity, M., Yamins, D. (eds.) ESOA 2006. LNCS, vol. 4335, pp. 28–49. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Istituto di Informatica e Telematica, IIT-CNR, Pisa, Italy

    Ilaria Matteucci

  2. Dipartimento di Matematica e Informatica, Università di Perugia, Perugia, Italy

    Francesco Santini

Authors
  1. Ilaria Matteucci
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesco Santini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Francesco Santini .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Milano, Crema, Italy

    Giovanni Livraga

  2. University of Skövde , Skövde, Sweden

    Vicenç Torra

  3. University of Urbino , Urbino, Italy

    Alessandro Aldini

  4. IIT National Research Council CNR , Pisa, Italy

    Fabio Martinelli

  5. Technische Universität Darmstadt , Darmstadt, Germany

    Neeraj Suri

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Matteucci, I., Santini, F. (2016). Decomposing Global Quantitative Properties into Local Ones. In: Livraga, G., Torra, V., Aldini, A., Martinelli, F., Suri, N. (eds) Data Privacy Management and Security Assurance. DPM QASA 2016 2016. Lecture Notes in Computer Science(), vol 9963. Springer, Cham. https://doi.org/10.1007/978-3-319-47072-6_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47072-6_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47071-9

  • Online ISBN: 978-3-319-47072-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation