2017
- Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision. Luca Laurenti, Alessandro Abate, Luca Bortolussi, Luca Cardelli, Milan Ceska and Marta Kwiatkowska. HSCC ’17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. Pittsburgh, Pennsylvania, USA — April 18 – 20, 2017. pp. 55-64.
- A computational approach to steady-state convergence of fluid limits for Coxian queuing networks with abandonment. Max Tschaikowski and Mirco Tribastone. Annals of Operations Research. May 2017, Volume 252, Issue 1, pp 101–120.
- Spatial fluid limits for stochastic mobile networks. Max Tschaikowski , Mirco Tribastone. Performance Evaluation. Volume 109, March 2017, Pages 52–76.
- ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations. L. Cardelli, M. Tribastone, M. Tschaikowski, and A. Vandin. In: Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17). Ed. by A. Legay and T. Margaria. Vol. 10206. LNCS. Springer, 2017.
- An experience in using machine learning for short-term predictions in smart transportation systems. Davide Bacciu, Antonio Carta, Stefania Gnesi, and Laura Semini. Journal of Logical and Algebraic Methods in Programming 87 (2017).
- Design and Optimisation of the FlyFast Front-end for Attribute-based Coordination. D. Latella and M. Massink. QAPL 2017. To appear in EPTCS
- FlyFast: A Mean Field Model Checker. D. Latella, M. Loreti and M. Massink. In A. Legay and T. Margaria (Eds.): TACAS 2017, Part II, LNCS 10206, pp. 303–309, 2017. DOI: 10.1007/978-3-662-54580-5_18
- Family-Based Model Checking with mCRL2. M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. In Proceedings of the 20th International Conference on Fundamental Approaches to Software Engineering (FASE’17), Uppsala, Sweden (M. Huisman and J. Rubin, eds.), Lecture Notes in Computer Science 10202, Springer, Berlin, 2017, 387-405. DOI: http://dx.doi.org/10.1007/978-3-662-54494-5_23
2016
- Programming of CAS Systems by Relying on Attribute-Based Communication. Yehia Abd Alrahman, Rocco De Nicola and Michele Loreti. ISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. Springer LNCS Volume 9952. pp 539-553.
- On the Power of Attribute-Based Communication. Yehia Abd Alrahman, Rocco De Nicola and Michele Loreti. FORTE 2016: Formal Techniques for Distributed Objects, Components, and Systems pp 1-18.
- Replicating Data for Better Performances in X10. Marina Andrić, Rocco De Nicola and Alberto Lluch Lafuente. In Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays. Lecture Notes in Computer Science Volume 9560. pp 236-251.
- Scaling Size and Parameter Spaces in Variability-aware Software Performance Models. M. Kowal, M. Tschaikowski, M. Tribastone, and I. Schaefer. In: Software Engineering 2016 – Fachtagung des GIFachbereichs Softwaretechnik. Ed. by J. Knoop and U. Zdun. Vol. 252. LNI. GI, 2016, pp. 33–34.
- Approximation of Probabilistic Reachability for Chemical Reaction Networks Using the Linear Noise Approximation. L. Bortolussi, L. Cardelli, M. Kwiatkowska, and L. Laurenti. In: Proceedings of the 13th International Conference on Quantitative Evaluation of Systems (QEST’16). Ed. by G. Agha and B. V. Houdt. Vol. 9826. LNCS. Springer, 2016, pp. 72–88.
- Variability-Based Design of Services for Smart Transportation Systems. M.H. ter Beek, A. Fantechi, S. Gnesi, and L. Semini. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verication and Validation: Discussion, Dissemination, Applications (ISoLA’16), Corfu, Greece (T. Margaria and B. Steen, eds.), Lecture Notes in Computer Science 9953, Springer, Berlin, 2016, 465-481.
DOI: http://dx.doi.org/10.1007/978-3-319-47169-3_38 - Location Aggregation of Spatial Population CTMC Models. L. Bortolussi, C. Feng. 14th international workshop on Quantitative Aspects on Programming Languages and systems (QAPL 2016).
- Probabilistic Modelling of Station Locations in Bicycle-Sharing Systems. D. Reijsbergen. In Software Technologies: Applications and Foundations, LNCS 9946, 83–97, 2016
- Adopting a Machine Learning Approach in the Design of Smart Transportation Systems. D. Bacciu, A. Carta, S. Gnesi, and L. Semini. ERCIM News 105: Special theme Planning and Logistics. April 2016.
- Supervisory Controller Synthesis for Product Lines using CIF 3. M.H. ter Beek, M.A. Reniers, and E.P. de Vink. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA’16), Corfu, Greece (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 9952, Springer, Berlin, 2016, 856 – 873.
- Statistical Model Checking for Product Lines. M.H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA’16), Corfu, Greece (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 9952, Springer, Berlin, 2016, 114 – 133.
- Transient and Steady-state Regime of a Family of List-based Cache Replacement Algorithms (extended version). N. Gast, B. Van Houdt. Queueing Systems: Theory and Applications (QUES)
- Are mean-field games the limits of finite stochastic games? with Josu Doncel and Bruno Gaujal. ACM MAMA Workshop, 2016.
- Construction of Lyapunov functions via relative entropy with application to caching. Nicolas Gast, ACM MAMA workshop 2016.
- Comparing Chemical Reaction Networks: A Categorical and Algorithmic Perspective. Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin. LICS 2016.
- Symbolic Computation of Differential Equivalences. Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin. POPL 2016.
- Efficient Syntax-driven Lumping of Differential Equations. Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin. TACAS 2016
- Quantitative Abstractions for Collective Adaptive Systems. Andrea Vandin, Mirco Tribastone. SFM 2016.
- Modeling and Analysis of Collective Adaptive Systems with CARMA and its Tools. M.Loreti and J.Hillston. SFM 2016, LNCS 9700, Springer 2016
- CARMA Eclipse plug-in: A tool supporting design and analysis of Collective Adaptive Systems. M. Loreti and J. Hillston. In Proceedings of 13th International Conference on Quantitative Evaluation of Systems (QEST), Quebec, Canada, August 2016
- Property-driven State-Space Coarsening for Continuous Time Markov Chains, M. Michaelides, D. Milios, J. Hillston and G. Sanguinetti, In Proceedings of 13th International Conference on Quantitative Evaluation of Systems (QEST), Quebec, Canada, August 2016.
- Rigorous graphical modelling of movement in Collective Adaptive Systems. N. Zon, S. Gilmore and J. Hillston. In Proceedings of ISOLA 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, LNCS 9952, pp. 674–688, Corfu, October 2016.
- Smoothed Model Checking for Uncertain Continuous Time Markov Chains. L. Bortolussi, D. Milios, G. Sanguinetti (2016). Information and Computation. 247, 235-253.
- Symbolic Performance Adaptation. E. Incerto, M. Tribastone, and C. Trubiani. SEAMS’16.
- Proceedings of the Workshop on FORmal methods for the quantitative Evaluation of Collective Adaptive SysTems. M.H. ter Beek and M. Loreti (eds.). (FORECAST’16). EPTCS 217, 2016.
- Hybrid Behaviour of Markov Population Models. L. Bortolussi (2016). Information and Computation. 247, 37-86.
- An experience in using machine learning for short-term predictions in smart transportation systems. Davide Bacciu, Antonio Carta, Stefania Gnesi, and Laura Semini. Journal of Logical and Algebraic Methods in Programming 87 (2017).
- A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems. V. Ciancia, D. Latella, M. Massink, R. Paskauskas, and A. Vandin. In T. Margaria and B. Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, volume 9952 of LNCS, pages 657-673. Springer-Verlag, 2016.
- Model Checking Spatial Logics for Closure Spaces. V. Ciancia, D. Latella, M. Loreti, and M. Massink. Logical Methods in Computer Science, 12(4):1-51, 2016. Published on line: 11 Oct. 2016. ISSN: 1860-5974.
- Moment-Based Probabilistic Prediction of Bike Availability for Bike-Sharing Systems. Cheng Feng, Jane Hillston, Daniël Reijsbergen, 13th International Conference on Quantitative Evaluation of Systems (QEST 2016), LNCS 9826, 139-155, Springer, 2016.
Bertinoro Summer School on Formal Methods for the Quantitive Evaluation of Collective Adaptive Systems
- Quantitative Abstractions for Collective Adaptive Systems. Andrea Vandin, Mirco Tribastone, SFM 2016, LNCS 9700, pp.202-232
- Spatial Logic and Spatial Model Checking for Closure Spaces. V. Ciancia, D. Latella, M. Loreti, M. Massink. SFM 2016, LNCS 9700, pp.156-201, Springer, 2016.
- Spatial Representations and Analysis Techniques. Vashti Galpin, SFM 2016, LNCS 9700, pp. 120-155
- Modelling and Analysis of Collective Adaptive Systems with CARMA and its Tools. Michele Loreti, Jane Hillston, SFM 2016, LNCS 9700, pp.83-119
- Mean-Field Limits Beyond Ordinary Differential Equations, Luca Bortolussi, Nicolas Gast, SFM 2016, LNCS 9700, pp. 61-82
- The Process Algebra for Located Markovian Agents and Scalable Analysis Techniques for the Modelling of Collective Adaptive Systems. Cheng Feng. PhD thesis. University of Edinburgh. 2016.
- Spatial and Stochastic Equivalence Relations for PALOMA. Paul Piho. Master of Science by Research dissertation, University of Edinburgh, 2016.
FORECAST Workshop
- From Collective Adaptive Systems to Human Centric Computation and Back: Spatial Model Checking for Medical Imaging. G. Belmonte, V. Ciancia, D. Latella, and M. Massink. FORECAST 2016. Vienna, Austria, 8 July 2016, Electronic Proceedings in Theoretical Computer Science 217, pp. 81–92.
- Stochastic and Spatial Equivalences for PALOMA. P. Piho and J. Hillston. FORECAST 2016. Vienna, Austria, 8 July 2016, Electronic Proceedings in Theoretical Computer Science 217, pp. 69–80.
- Challenges in Quantitative Abstractions for Collective Adaptive Systems. M. Tribastone. FORECAST 2016. Vienna, Austria, 8 July 2016, Electronic Proceedings in Theoretical Computer Science 217, pp. 62–68.
- On Formal Methods for Collective Adaptive System Engineering. Scalable Approximated, Spatial Analysis Techniques. Extended Abstract. D. Latella. FORECAST 2016. Vienna, Austria, 8 July 2016, Electronic Proceedings in Theoretical Computer Science 217, pp. 53–61.
- Modelling movement for collective adaptive systems with CARMA. N. Zoń, V. Galpin, and S. Gilmore. FORECAST 2016. Vienna, Austria, 8 July 2016, Electronic Proceedings in Theoretical Computer Science 217, pp. 43–52.
- Data as processes: introducing measurement data into CARMA models. S. Gilmore. FORECAST 2016, Vienna, Austria, 8 July 2016, Electronic Proceedings in Theoretical Computer Science 217, pp. 31–42.
- On-the-fly Mean-field Model-checking for Attribute-based Coordination. V. Ciancia, D. Latella, M. Massink. COORDINATION 2016, LNCS 9686, pp. 67-83, Springer.
- Modelling Ambulance Deployment with CARMA. Vashti Galpin. COORDINATION 2016, LNCS 9686, pp.121-137, Springer.
- Automatic Moment-Closure Approximation of Spatially Distributed Collective Adaptive Systems. Cheng Feng, Jane Hillston, Vashti Galpin: ACM Trans. Model. Comput. Simul. 26(4): 26 (2016)
- Towards a Feature mu-Calculus Targeting SPL Verification. M.H. ter Beek, E.P. de Vink, and T.A.C. Willemse. In Proceedings of the 7th International Workshop on Formal Methods and Analysis for Software Product Line Engineering (FMSPLE’16), Eindhoven, The Netherlands (J. Rubin and T. Thüm, eds.), Electronic Proceedings in Theoretical Computer Science 206, arXiv:1604.00350v1 [cs.LO], 2016, 61-75.
DOI: http://dx.doi.org/10.4204/EPTCS.206.6 - Modelling and Analysing Variability in Product Families: Model
Checking of Modal Transition Systems with Variability Constraints. M.H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti, Journal of Logical and Algebraic Methods in
Programming 85, 2 (2016), 287-315. DOI: 10.1016/j.jlamp.2015.11.006
2015
- Scaling Size and Parameter Spaces in Variability-aware Software Performance Models. M. Kowal, M. Tschaikowski, M. Tribastone, and I. Schaefer. In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE’15). Ed. by M. B. Cohen, L. Grunske, and M. Whalen. Vol. 252. LNI. IEEE Computer Society, 2015, pp. 407–417.
- Efficient Checking of Individual Rewards Properties in Markov Population Models. L. Bortolussi and J. Hillston. In: Proceedings 13th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL’15). Ed. by N. Bertrand and M. Tribastone. Vol. 194. EPTCS. 2015, pp. 32–47.
- E. Bartocci, L. Bortolussi, D. Milios, L. Nenzi, and G. Sanguinetti. Studying Emergent Behaviours in Morphogenesis Using Signal Spatio-Temporal Logic. In: Hybrid Systems Biology – Revised Selected Papers of the 4th International Workshop on Hybrid Systems Biology (HSB’15). Ed. by A. Abate and D. Safránek. Vol. 9271. LNCS. Springer, 2015, pp. 156–172.
- E. Bartocci, L. Bortolussi, L. Nenzi, G. Sanguinetti (2015). System Design of Stochastic Models using Robustness of Temporal Properties. Theoretical Computer Science. 587: 3-25.
- Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically. D. Latella, M. Massink and E. de Vink. Logical Methods in Computer Science (LMCS), Vol. 11(4:16)2015 p 1–40. DOI:10.2168/LMCS-11(4:16)2015
- An experimental spatio-temporal model checker. Vincenzo Ciancia, Gianluca Grilletti, Diego Latella, Michele Loreti and Mieke Massink. In Proceedings of VERY*SCART 2015. LNCS 9509. DOI:10.1007/978-3-662-49224-6 24
- Towards Automatic Decision Support for Bike-Sharing System Design. M. H. ter Beek, S. Gnesi, D. Latella, and M. Massink. Software Engineering and Formal Methods – Revised selected papers of the SEFM 2015 collocated workshops: ATSE, HOFM, MoKMaSD, and VERY*SCART, York, UK (D. Bianculli, R. Calinescu, and B. Rumpe, eds.), Lecture Notes in Computer Science 9509, Springer, Berlin, 2015, 266 – 280.
- S. Gilmore and D. Reijsbergen. Validation of Automatic Vehicle Location Data in Public Transport Systems. Electronic Notes in Theoretical Computer Science
Volume 318, 25 November 2015, Pages 31–51. DOI: 10.1016/j.entcs.2015.10.018 - D. Latella, M. Loreti, and M. Massink. On-the-fly Fluid Model Checking via Discrete Time Population Models. In M. Beltrán, W. Knottenbelt, and J. Bradley, editors, Computer Performance Engineering, volume 9272 of LNCS, pages 193–207. Springer-Verlag, 2015. ISSN: 0302-9743, DOI: 10.1007/978-3-319-23267-6_13.
- D. Latella, M. Massink, and E. de Vink. A Definition Scheme for Quantitative Bisimulation. In N. Bertrand and M. Tribastone, editors, Proceedings of the Thirteenth Workshop on Quantitative Aspects of Programming Languages (QAPL 2015), volume 194 of Electronic Proceedings in Theoretical Computer Science, pages 63–78.
EPTCS, 2015. DOI:10.4204/EPTCS.194.5. - Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente and Andrea Vandin. Modelling and Analyzing Adaptive Self-assembly Strategies with Maude. Science of Computer Programming, Volume 99, 1 March 2015, Pages 75–94. DOI: 10.1016/j.scico.2013.11.043
- Giulio Iacobelli, Mirco Tribastone and Andrea Vandin. Differential Bisimulation for a Markovian Process Algebra. Mathematical Foundations of Computer Science 2015
Volume 9234 of the series Lecture Notes in Computer Science pp 293-306. DOI: 10.1007/978-3-662-48057-1_23 - C.Feng, M. Gribaudo and J. Hillston. Performance Analysis of Collective Adaptive Behaviour in Time and Space. Proceedings of UK Performance Engineering Workshop 2014. ENTCS Volume 318, pp. 53–68, November 2015. DOI: 10.1016/j.entcs.2015.10.019
- S.Gilmore, J.Hillston and M.Tribastone. Service Composition for Collective Adaptive Systems. Software, Services and Systems. LNCS 8950, pp. 490–505. DOI: 10.1007/978-3-319-15545-6_28
- Jane Hillston and Michele Loreti. Specification and Analysis of Open-Ended Systems with CARMA. Agent Environments for Multi-Agent Systems IV
Volume 9068 of the series Lecture Notes in Computer Science pp 95-116. November 2015. DOI: 10.1007/978-3-319-23850-0_7 - Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, and Franco Mazzanti,
Modelling and analysing variability in product families: Model checking of modal
transition systems with variability constraints. To appear in the Journal of Logical
and Algebraic Methods in Programming, Elsevier Science Publishers, Amsterdam. DOI: http://dx.doi.org/10.1016/j.jlamp.2015.11.006 - Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, Mieke Massink. Qualitative and Quantitative Monitoring of Spatio-Temporal Properties, Vol 9333 of the series Lecture Notes in Computer Science pp 21-37, Springer 2015
- A Partial-differential Approximation for Spatial Stochastic Process Algebra, ACM Digital Library, ICST, Feb 2015.
- M. Tschaikowski and M. Tribastone. Approximate reduction of heterogenous nonlinear models with differential hulls. In: IEEE TAC (2015).
- Daniël Reijsbergen, Werner Scheinhardt and Pieter-Tjerk de Boer. A sequential hypothesis test based on a generalized Azuma inequality. Statistics and Probability Letters
- D. Latella, M. Loreti, M. Massink and V. Senni. On StocS: A Stochastic Extension of SCEL. In R. De Nicola and R. Hennicker (Eds.) Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. LNCS 8950. Springer, 2015.
- Latella D, Loreti M, Massink M. Investigating Fluid-Flow Semantics of Asynchronous Tuple-Based Process Languages for Collective Adaptive Systems, COORDINATION 2015. LNCS 9037 19 – 34.
- A. Pourranjbar. Performance Analysis of Large-Scale Resource-Bound Computer Systems PhD thesis, University of Edinburgh, graduated June 2015.
- M. H. ter Beek, S. Gnesi, and F. Mazzanti. Model Checking Value-Passing Modal Specifications. In Perspectives of System Informatics – Revised selected papers of the 9th International Ershov Informatics Conference (PSI’14), St. Petersburg, Russia (A. Voronkov and I. Virbitskaite, eds.), Lecture Notes in Computer Science 8974, Springer, Berlin, 2015, 304-319. URL: http://dx.doi.org/10.1007/978-3-662-46823-4_25
- M. H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin. Quantitative Analysis of Probabilistic Models of Software Product Lines with Statistical Model Checking. In Proceedings of the 6th International Workshop on Formal Methods for Software Product Line Engineering (FMSPLE’15), London, UK (J. M. Atlee and S. Gnesi, eds.), Electronic Proceedings in Theoretical Computer Science 182, arXiv:1504.03476v1 [cs.LO], 2015, 56-70. URL: http://dx.doi.org/10.4204/EPTCS.182.5
- Ezio Bartocci, Luca Bortolussi, Laura Nenzi, Guido Sanguinetti: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587: 3-25 (2015).http://dx.doi.org/10.1016/j.tcs.2015.02.046
- M. Massink and R. Paskauskas. Model-based Assessment of Aspects of User-satisfaction in Bicycle Sharing Systems. IEEE International Conference on Intelligent Transportation Systems (ITSC15), September 2015.
- Vincenzo Ciancia, Diego Latella, Mieke Massink and Rytis Paskauskas. Exploring Spatio-Temporal Properties of Bike-sharing Systems. First International Workshop on Spatial and COllective PErvasive Computing Systems (SCOPES). Workshop at IEEE SASO 2015, located at MIT, Cambridge, USA; September 21, 2015.
- M. Tschaikowski and M. Tribastone. A unified framework for differential aggregations in Markovian process algebra. In: J. Logic Algebra. Methods Program. 84.2 (2015), pp. 238–258. ISSN: 2352- 2208.
DOI: http://dx.doi.org/10.1016/j.jlamp.2014.10.004. URL: https://dl. dropboxusercontent.com/u/13100903/papers/jlamp15.pdf. - D. Latella, M. Loreti, M. Massink. On-the-fly PCTL Fast Mean-Field Approximated Model-Checking for Self-organising Coordination. Science of Computer Programming. Elsevier, 110:23–50, 2015. DOI: 10.1016/j.scico.2015.06.009.
- Cheng Feng and Jane Hillston. Speed-up of Stochastic Simulation of PCTMC Models by Statistical Model Reduction. EPEW 15. Vol. 9272. LNCS. Springer, 2015, pp. 291–305.
- L. Cardelli, M. Tribastone, M. Tschaikowski, A. Vandin. Forward and Backward Bisimulations for Chemical Reaction Networks. 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015. Ed. by L. Aceto and D. de Frutos-Escrig. Vol. 42. LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 2015, pp. 226–239. DOI: 10.4230/LIPIcs. CONCUR.2015.226. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.226
- M. H. ter Beek, A. Legay, A. Lluch Lafuente, and A. Vandin. Statistical Analysis of Probabilistic Models of Sofware Product Lines with Quantitative Constraints. In Proceedings of the 19th International Software Product Line Conference (SPLC’15), Nashville, TN, USA, ACM, New York, 2015, 11-15. DOI: http://dx.doi.org/10.1145/2791060.2791087
- M. H. ter Beek, F. Damiani, S. Gnesi, F. Mazzanti, and L. Paolini. From Featured Transition Systems to Modal Transition Systems with Variability Constraints. In Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM’15), York, UK (R. Calinescu and B. Rumpe, eds.), Lecture Notes in Computer Science 9276, Springer, Berlin, 2015, 344-359. URL: http://dx.doi.org/10.1007/978-3-319-22969-0_24
- M. H. ter Beek, A. Fantechi, and S. Gnesi. Applying the Product Lines Paradigm to the Quantitative Analysis of Collective Adaptive Systems. In Proceedings of the 19th International Software Product Line Conference (SPLC’15), Nashville, TT, USA, ACM, New York, 2015, 321-326. URL: http://dx.doi.org/10.1145/2791060.2791100
- Davide Bacciu, Stefania Gnesi and Laura Semini, Using a Machine Learning Approach to Implement and Evaluate Product Line Features. In Proceedings 11th International Workshop on Automated Specification and Verification of Web Systems (WWV’15), Oslo, Norway (M.H. ter Beek and A. Lluch Lafuente, eds.), Electronic Proceedings in Theoretical Computer Science 188, 2015, 75-83. URL: http://dx.doi.org/10.4204/EPTCS.188.8
- M. H. ter Beek, A. Fantechi, S. Gnesi, and F. Mazzanti. Using FMC for Family-Based Analysis of Software Product Lines. In Proceedings of the 19th International Software Product Line Conference (SPLC’15), Nashville, TN, USA, ACM, New York, 2015, 432-436. URL: http://dx.doi.org/10.1145/2791060.2791118
- Nicolas Gast, The Power of Two Choices on Graphs: the Pair-Approximation is Accurate. ACM MAMA Workshop. Perf. Eval. Review.Volume 43 Issue 2, September 2015, Pages 69-71, ACM New York, NY, USA. DOI: 10.1145/2825236.2825263.
- Nicolas Gast, Guillaume Massonnet, Daniël Reijsbergen, and Mirco Tribastone. Probabilistic Forecasts of Bike-Sharing Systems for Journey Planning.Proceedings of the 24th ACM International on Conference on Information and Knowledge Management,Pages 703-712, ACM New York, 2015. DOI: 10.1145/2806416.2806569
- M. H. ter Beek, S. Gnesi, and F. Mazzanti. Model Checking Value-Passing Modal Specifications. In Perspectives of System Informatics – Revised selected papers of the 9th International Ershov Informatics Conference (PSI’14), St. Petersburg, Russia (A. Voronkov and I. Virbitskaite, eds.), Lecture Notes in Computer Science 8974, Springer, Berlin, 2015, 304-319.
- T. Belder, M. H. ter Beek, and E. P. de Vink. Coherent branching feature bisimulation. In Proceedings of the 6th International Workshop on Formal Methods for Software Product Line Engineering (FMSPLE’15), London, UK (J. M. Atlee and S. Gnesi, eds.), Electronic Proceedings in Theoretical Computer Science 182, arXiv:1504.03474v1 [cs.LO], 2015, 14-30.
- Luca Bortolussi, Jane Hillston. Model checking single agent behaviours by fluid approximation. Inf. Comput. 242: 183226 (2015).
- N Gast, B Van Houdt, Transient and Steady-state Regime of a Family of List-based Cache Replacement Algorithms – Proceedings of the 2015 ACM SIGMETRICS
- Ezio Bartocci, Luca Bortolussi, Laura Nenzi, Guido Sanguinetti, System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587: 3-25 (2015).
- Luca Bortolussi, Rocco de Nicola, Vashti Galpin, Stephen Gilmore, Jane Hillston, Diego Latella, Michele Loreti, and Mieke Massink, CARMA: Collective Adaptive Resource-sharing Markovian Agents, N. Bertrand and M. Tribastone (Eds.): QAPL 2015 EPTCS 194, 2015, pp. 16–31, DOI: 10.4204/EPTCS.194.2
2014
- Latella D, Loreti M, Massink M, Senni V. 2014. Stochastically timed predicate-based communication primitives for autonomic computing. QAPL 2014. EPTCS 154:1-16. DOI:10.4204/EPTCS.154.1
- Reijsbergen D, de Boer P-T, Scheinhardt W, Haverkort BR. 2014. On Hypothesis Testing for Statistical Model Checking.
- Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
Marco Bernardo, Rocco De Nicola and Michele Loreti. - Finding optimal timetables for Edinburgh bus routes. Ludovica Luisa Vissat, Allan Clark and Stephen Gilmore. Seventh International Workshop on Practical Applications of Stochastic Modelling (PASM 2014), Newcastle, England, May 2014.
- Patch-based modelling of city-centre bus movement with phase-type distributions. Daniël Reijsbergen, Stephen Gilmore, and Jane Hillston. Seventh International Workshop on Practical Applications of Stochastic Modelling (PASM 2014), Newcastle, England, May 2014.
- PALOMA: A Process Algebra for Located Markovian Agents. Cheng Feng and Jane Hillston. 11th International Conference on Quantitative Evaluation of Systems (QEST 2014), Florence, Italy, 8-10th September 2014
- Probabilistic Programming Process Algebra. Anastasis Georgoulas, Jane Hillston, Dimitrios Milios and Guido Sanguinetti. 11th International Conference on Quantitative Evaluation of Systems (QEST 2014), Florence, Italy, 8-10th September 2014
- Specifying and Monitorig Properties of Stochastic Spatio-Temporal Systems in Signal Temporal Logic, L. Bortolussi, L. Nenzi. 8th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS 2014)
- M.H. ter Beek, A. Fantechi, and S. Gnesi, Challenges in Modelling and Analyzing Quantitative Aspects of Bike-Sharing Systems. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14), Corfu, Greece (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 8802, Springer, Berlin, 2014, 351 – 367. DOI: http://dx.doi.org/10.1007/978-3-662-45234-9_25
- M.H. ter Beek and E.P. de Vink, Towards Modular Verification of Software Product Lines with mCRL2. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14), Corfu, Greece (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 8802, Springer, Berlin, 2014, 368 – 385. DOI: http://dx.doi.org/10.1007/978-3-662-45234-9_26
- Latella D, Loreti M, Massink M, 2014. On-the-fly Probabilistic Model Checking ICE 2014. EPTCS 166: 45 – 59.
- Maurice ter Beek, Luca Bortolussi, Vincenzo Ciancia, Stefania Gnesi, Jane Hillston, Diego Latella and Mieke Massink, A quantitative approach to the design and analysis of collective adaptive systems for smart cities. ERCIM news 98 – special theme: Smart Cities. July 2014. http://ercim-news.ercim.eu/en98/special/a-quantitative-approach-to-the-design-and-analysis-of-collective-adaptive-systems-for-smart-cities
- Distributed Statistical Analysis of Complex Systems Modeled Through a Chemical Metaphor. Danilo Pianini, Stefano Sebastio, and Andrea Vandin. 5th International Workshop on Modeling and Simulation of Peer-to-Peer and Autonomic Systems (MOSPAS 2014)
- Stochastic Approximation of Global Reachability Probabilities of Markov Population Models. Luca Bortolussi, Roberta Lanciani. EPEW 2014: 224-239.
- Data-Driven Statistical Learning of Temporal Logic Properties. Ezio Bartocci, Luca Bortolussi, Guido Sanguinetti. FORMATS 2014: 23-37.
- Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients. Sara Bufo, Ezio Bartocci, Guido Sanguinetti, Massimo Borelli, Umberto Lucangelo, Luca Bortolussi. ISoLA (2) 2014: 391-403.
- A Statistical Approach for Computing Reachability of Non-linear and Stochastic Dynamical Systems. Luca Bortolussi, Guido Sanguinetti. QEST 2014: 41-56.
- Mean-Field Approximation and Quasi-Equilibrium Reduction of Markov Population Models. Luca Bortolussi, Rytis Paskauskas. QEST 2014: 106-121.
- Challenges for Quantitative Analysis of Collective Adaptive Systems, Jane Hillston, Trustworthy Global Computing – 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers. Springer 2014 Lecture Notes in Computer Science, pp.14-21.
- On-the-fly Fast Mean-Field Model-Checking, Diego Latella, Michele Loreti, and Mieke Massink, Trustworthy Global Computing – 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers. Springer 2014 Lecture Notes in Computer Science, pp.297-314. An extended version of this paper is available as arXiv:1312.3416 [cs.LO].
- Hybrid semantics for Bio-PEPA, Vashti Galpin, Information and Computation, Volume 236, pp.122-145, 2014. DOI: 10.1016/j.ic.2014.01.016
- A capacity planning tool for PEPA, Christopher D Williams, Master of Informatics dissertation, The University of Edinburgh, 2014.
- Fluid Performability Analysis of Nested Automata Models, Luca Bortolussi, Jane Hillston, and Mirco Tribastone. Proceedings of the Seventh International Workshop on Practical Applications of Stochastic Modelling (PASM 2014), Newcastle, England, May 2014.
- Incentives and redistribution in homogeneous bike-sharing systems with stations of finite capacity. Christine Fricker and Nicolas Gast. EURO Journal on Transportation and Logistics. page 1-31. Springer. 2014. DOI: 10.1007/s13676-014-0053-5
- Impact of demand-response on the efficiency and prices in real-time electricity markets. Nicolas Gast, Jean-Yves Le Boudec, and Dan-Cristian Tomozei. 2014. In Proceedings of the 5th international conference on Future energy systems (e-Energy ’14). ACM, New York, NY, USA, 171-182. DOI: 10.1145/2602044.2602052
- Optimal Generation and Storage Scheduling in the Presence of Renewable Forecast Uncertainties. Gast, N.; Tomozei, D.-C.; Le Boudec, J.-Y., Smart Grid, IEEE Transactions on , vol.5, no.3, pp.1328,1339, May 2014. doi: 10.1109/TSG.2013.2285395
- Extended Differential Aggregations in Process Algebra for Performance and Biology, Max Tschaikowski and Mirco Tribastone, Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, EPTCS 154, pp.34-47, Grenoble, France, 12-13 April 2014. DOI: 10.4204/EPTCS.154.3
- Patch-based Hybrid Modelling of Spatially Distributed Systems by Using Stochastic HYPE – ZebraNet as an Example, Cheng Feng, Proceedings of QAPL 2014, EPTCS 154, 2014, pp. 64-77, DOI: 10.4204/EPTCS.154.5.
- Automated Capacity Planning for PEPA Models, Christopher D. Williams and Jane Hillston. A. Horváth and K. Wolter (Eds.): EPEW 2014, LNCS 8721, pp. 209–223, 2014.
- Formal Punctuality Analysis of Frequent Bus Services Using Headway Data, Daniël Reijsbergen and Stephen Gilmore. A. Horváth and K. Wolter (Eds.): EPEW 2014, LNCS 8721, pp. 164–178, 2014.
- An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems, Andrea Vandin, Mirco Tribastone and Stephen Gilmore. E. Albert and E. Sekerinski (Eds.): IFM 2014, LNCS 8739, pp. 71–86, 2014.
- The Benefits of Sometimes Not Being Discrete, Jane Hillston. In P. Baldan and D. Gorla (Eds.): Proceedings of the 25th International Conference on Concurrency Theory (CONCUR’14), Rome, Italy, Springer LNCS 8704, pp. 7–22, 2014.
- Specifying and verifying properties of space. Vincenzo Ciancia, Diego Latella, Michele Loreti, Mieke Massink. 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Pages 222-235. Volume 8705. Lecture Notes in Computer Science. Springer.
- Using mCRL2 for the Analysis of Software Product Lines. M.H. ter Beek and E.P. de Vink. In Proceedings of the 2nd FME Workshop on Formal Methods in Software Engineering (FormaliSE’14), Hyderabad, India, IEEE Computer Society, Los Alamitos, CA, 2014, 31 – 37. DOI: http://dx.doi.org/10.1145/2593489.2593493
- VMC: Recent Advances and Challenges Ahead. M.H. ter Beek and F. Mazzanti. In Proceedings of the First Workshop on Software Product Line Analysis Tools (SPLat’14), Volume 2 of the Proceedings of the 18th International Software Product Line Conference (SPLC’14), Florence, Italy, ACM Press, New York, 2014, 70 – 77. DOI: http://dx.doi.org/10.1145/2647908.2655969
- Software Product Line Analysis with mCRL2. M.H. ter Beek and E.P. de Vink. In Proceedings of the First Workshop on Software Product Line Analysis Tools (SPLat’14), Volume 2 of the Proceedings of the 18th International Software Product Line Conference (SPLC’14), Florence, Italy, ACM Press, New York, 2014, 78 – 85. DOI: http://dx.doi.org/10.1145/2647908.2655970
- Towards Modular Verification of Software Product Lines with mCRL2. M.H. ter Beek and E.P. de Vink. In Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’14), Corfu, Greece (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 8802, Springer, Berlin, 2014, 368 – 385. DOI: http://dx.doi.org/10.1007/978-3-662-45234-9_26
- Family-Based Performance Analysis of Variant-Rich Software Systems. Matthias Kowal, Ina Schaefer and Mirco Tribastone. Fundamental Approaches to Software Engineering (FASE’14), Lecture Notes in Computer Science 8411, 2014, 94–108. DOI: http://dx.doi.org/10.1007/978-3-642-54804-8_7
- Efficient Optimization of Software Performance Models via Parameter-Space Pruning. Mirco Tribastone. 5th ACM/SPEC International Conference on Performance Engineering (ICPE’14). Dublin, Ireland. March 2104. pp.63–73. DOI: 10.1145/2568088.2568090
- Behavioral Relations in a Process Algebra for Variants. Mirco Tribastone. Proceedings of the 18th International Software Product Line Conference – Volume 1 (ACM SPLC’14). ACM. New York, NY, USA. pp.82–91. DOI: 10.1145/2648511.2648520
- Blending randomness in closed queueing network models. Giuliano Casale, Mirco Tribastone and Peter G. Harrison. Performance Evaluation, 2014. DOI: http://dx.doi.org/10.1016/j.peva.2014.09.001
- Dimming Relations for the Efficient Analysis of Concurrent Systems via Action Abstraction. Giulio Iacobelli, Rocco De Nicola and Mirco Tribastone. International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE’14). Springer LNCS 8641, pp.216–231. 2014. DOI: 10.1007/978-3-662-43613-4_14
- On-the-fly Probabilistic Model Checking, Diego Latella, Michele Loreti and Mieke Massink, In Ivan Lanese, Alberto Lluch Lafuente, Ana Sokolova and Hugo Torres Vieira: Proceedings 7th Interaction and Concurrency Experience (ICE 2014), Berlin, Germany, 6th June 2014, Electronic Proceedings in Theoretical Computer Science 166, pp. 45–59.
- Data verification for collective adaptive systems: spatial model-checking of vehicle location data, Vincenzo Ciancia, Stephen Gilmore, Diego Latella, Michele Loreti, and Mieke Massink, Proceedings of the IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops (FoCAS@SASO’14), IEEE Computer Society, 2014. DOI: 10.1109/SASOW.2014.16
- Modelling residential smart energy schemes. Vashti Galpin, Proceedings of the IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops (FoCAS@SASO’14), IEEE Computer Society, 2014.
- Two Possibly Alternative Approaches to the Semantics of Stochastic Process Calculi. De Nicola R, Latella D, Loreti M, and Massink M. In Abadi M., Gardner P., Gordon A.D., and Mardare R. (Eds) Essays for Luca Cardelli Fest. Microsoft Research Technical Report MSR-TR-2014-104. 2014.
2013
- Flyer for public use with user communities, QUANTICOL Deliverable D6.4.
- Bortolussi L, Hayden R. 2013. Bounds on the deviation of discrete-time Markov chains from their mean-field model. Performance Evaluation. 70(10):736-749. DOI 10.1016/j.peva.2013.08.012
- Bortolussi L, Sanguinetti G. 2013. Learning and designing stochastic processes from logical constraints. 10th International Conference on Quantitative Evaluation of SysTems, QEST 2013. LNCS 8054:89-105. DOI: 10.1007/978-3-642-40196-1_7
- Bortolussi L, Lanciani R. 2013. Model Checking Markov Population Models by Central Limit Approximation. 10th International Conference on Quantitative Evaluation of SysTems, QEST 2013. LNCS 8054:123-138. DOI: 10.1007/978-3-642-40196-1_9
- Stochastic Process Algebra and Stability Analysis of Collective Systems, Luca Bortolussi, Diego Latella, Mieke Massink, Proceedings of the 15th International Conference on Coordination Models and Languages, COORDINATION 2013, R. De Nicola and C. Julien (Eds.), LNCS 7890, pp.1-15, 2013.
- A Quantitative Approach to the Design and Analysis of Collective Adaptive Systems, Luca Bortolussi, Rocco De Nicola, Nicolas Gast, Stephen Gilmore, Jane Hillston, Mieke Massink, Mirco Tribastone, 1st FoCAS Workshop on Fundamentals of Collective Systems, Taormina, Sicily, Italy, Sept 2013.
- On the Robustness of Temporal Properties for Stochastic Models. Ezio Bartocci, Luca Bortolussi, Laura Nenzi and Guido Sanguinetti, Proceedings Second International Workshop on Hybrid Systems and Biology. EPTCS 125:3-19. September 2013.
- Interaction and Observation: Categorical Semantics of Reactive Systems through Dialgebras, Vincenzo Ciancia, Proceedings of the 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013, Reiko Heckel, Stefan Milius (Eds.), LNCS 8089, pp.110-125, 2013.
- ABC–Fun: A Probabilistic Programming Language for Biology, Anastasis Georgoulas, Jane Hillston and Guido Sanguinetti, Eleventh Conference on Computational Methods in Systems Biology, Lecture Notes in Computer Science Volume 8130, 2013, pp 150-163.
- Bounds on the deviation of discrete-time Markov chains from their mean-field model. Luca Bortolussi and Richard Hayden, Performance Evaluation. 70(10):736-749. 2013.
- Learning and designing stochastic processes from logical constraints. Luca Bortolussi and Guido Sanguinetti. 10th International Conference on Quantitative Evaluation of SysTems, QEST 2013. LNCS 8054:89-105. 2013.
- Model Checking Markov Population Models by Central Limit Approximation. Luca Bortolussi and Roberta Lanciani,. 10th International Conference on Quantitative Evaluation of SysTems, QEST 2013. LNCS 8054:123-138. 2013.
- Constraint design rewriting, Roberto Bruni, Alberto Lluch Lafuente, Ugo Montanari, Science of Computer Programming, Available online 13 November 2013, ISSN 0167-6423.
- An Aggregation Technique for Large-Scale PEPA Models with Non-Uniform Populations, Alireza Pourranjbar and Jane Hillston, 7th International Conference on Performance Evaluation Methodologies and Tools, Torino, Italy, December 2013. DOI: 10.4108/icst.valuetools.2013.254397
- Contextual Lumpability, Jane Hillston, Andrea Marin, Carla Piazza and Sabina Rossi, 7th International Conference on Performance Evaluation Methodologies and Tools, Torino, Italy, December 2013. DOI: 10.4108/icst.valuetools.2013.254408
- Differential Analysis of Interacting Automata with Immediate Actions. Luca Bortolussi and Mirco Tribastone, 7th International Conference on Performance Evaluation Methodologies and Tools, Torino, Italy, December 2013. DOI: 10.4108/icst.valuetools.2013.254364
- Modelling and analyzing adaptive self-assembly strategies with Maude, Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin, Science of Computer Programming, Available online 14 December 2013, ISSN 0167-6423.
- Combining declarative and procedural views in the specification and analysis of product families, Maurice H. ter Beek, Alberto Lluch Lafuente, and Marinella Petrocchi, In Proceedings of the 17th International Software Product Line Conference co-located workshops (SPLC ’13 Workshops). ACM, New York, NY, USA, 10-17. 2013.
- Insensitivity to Service-time Distributions for Fluid Queueing Models, Max Tschaikowski and Mirco Tribastone, 7th International Conference on Performance Evaluation Methodologies and Tools, Torino, Italy, December 2013. DOI: 10.4108/icst.valuetools.2013.254374
- MultiVeStA: Statistical Model Checking for Discrete Event Simulators, Stefano Sebastio and Andrea Vandin, 7th International Conference on Performance Evaluation Methodologies and Tools, Torino, Italy, December 2013. DOI: 10.4108/icst.valuetools.2013.25437