Sensor networks, internet of things and smart environments
Title: Sensor networks, internet of things and smart environments
Lecturer: Michele Girolami (CNR Pisa), Alexander Kocian (Dipartimento di Informatica), Stefano Chessa (Dipartimento di Informatica)
Period: 26, 27,28 Aprile (ore 11:00-13:00) – 2,3,4,5,6 Maggio (ore 11:00-13:00) – 9-10 Maggio (ore 11:00-13:00)
Place: Sala Riunioni OVEST Dip.to Informatica
- Wireless sensors: issues and requirements
- Architectures and MAC protocols
- Localization and routing
- Energy harvesting and energy management
- Smart environments
- ZigBee and Bluetooth
Searching by Similarity on a Very Large Scale
Title: Searching by Similarity on a Very Large Scale
Lecturer: Giuseppe Amato, CNR Pisa
Period: 4 – 15 July 2016, 11.00 – 13.00
- Foundation of Metric Space Searching
- Distance Searching Problem
- Metric Distance Measures
- Similarity Queries
- Basic Partitioning Principles
- Principles of Similarity Query Execution
- Policies for avoiding Distance Computations
- Metric Space Transformations
- Priciples of Approximate Similarity Search
- Advanced issues: Statistics, Proximity, Performance Prediction, Tree quality measures
- Advanced issues: Choosing reference points
- Exact Similarity Search
- Vantage Point Trees
- The M-Tree Family
- The M-Tree
- Bulk-Loading Algorithm
- Multy-Way Insertion Algorithms
- The Slim Tree
- Slim-Down Algorithm
- Pivoting M-Tree
- Hash Based Methods
- Approximate Similarity Search with M-Tree
- Relative Error Approximation
- Good Fraction Approximation
- Small Chance Improvement Approximation
- Proximity-Based Approximation
- PAC Nearest Neighbor Searching
- Performance tests
- Other Approximate Similarity Search Methods
- Permutation Based Methods
- Permutation Spearman Rho
- Locality Sensitive Hashing (LSH)
- LSH based on p-stable distributions
- LSH with Hamming Distance
Introduction to process calculi and related type systems
Title: Introduction to process calculi and related type systems
Lecturer: Ilaria Castellani, Rosario Pugliese
Period: 1, 2, 3, 9, 10, 11, 14, 15, 16, 17 december 2015, 14.30 — 16.30
Place: Università di Firenze, Viale Morgagni, Aula Anfiteatro
This course aims at introducing, and motivating the use of, some basic formal methods from Concurrency Theory. It is split in two parts. Firstly, some well-known process calculi, e.g. CCS and pi-calculus, are presented together with the most commonly used techniques for defining their operational and observational semantics. Then, many type systems are presented for ensuring different properties of distributed and concurrent processes, such as e.g. correctness of interaction and security.
Lectures & topics:
1. CCS: syntax and operational semantics. Observational semantics. Trace equivalence.
2. Strong & weak bisimilarity. Axiomatic alternative characterisation. Reduction semantics & barbed bisimilarity. Coincidence result. Link mobility. Introduction to pi-calculus.
3. Pi-calculus: syntax and operational semantics. Reduction semantics. Polyadic variant and its encoding. Data encoding: boolean values and operators.
4. Early & late operational semantics. Observational semantics: late bisimilarity, early bisimilarity, barbed congruence. Coincidence result.
5. Introduction to type systems for the pi-calculus: Milner’s sorting & I/O typing by Pierce and Sangiorgi.
6. An advanced type system: Kobayashi’s usage types.
7. Binary session calculi and associated type systems.
8. Multiparty session calculi and associated type systems.
9. Type systems for security: the linear pi-calculus & enhanced session types.
10. Session calculi with monitoring and adaptation.
Specification and Verification of Complex Business Processes
ATTENTION: The course is canceled
Title: Specification and Verification of Complex Business Processes
Lecturer: Kamel Barkaoui (Conservatoire National des Arts et Métiers, Parigi)
Period: 12 -23 September 2016
The Business Process Modeling Notation (BPMN) has been widely used as a tool for business process modeling. However, BPMN suffers from a lack of standard formal semantics. This weakness can lead to inconsistencies, ambiguities, and incompletenesses within the developed models.
In this course we propose a formal semantics of BPMN using recursive ECATNets. Owing to this formalism, a large set of BPMN features such cancellation, multiple instantiation of subprocesses and exception handling can be covered while taking into account the data flow aspect. The benefits and usefulness of this modelling are illustrated through two examples.
Moreover, since recursive ECATNets semantics is expressed in terms of conditional rewriting logic, one can use the Maude LTL model checker to verify several behavioral properties related to BPMN models.
Coalgebre, automi e linguaggi nominali ecc
Title: Coalgebre, automi e linguaggi nominali ecc
Lecturer: Bartek Klin
Period: Monday June 27, 11:00-13:00; Tuesday June 28, 10:00-13:00; Thursday June 30, 10:00-13:00; Thursday June 30, 16:00-18:00 – always in Aula Seminari Ovest
Title: A bialgebraic approach to Structural Operational Semantics
Structural Operational Semantics (SOS) is a simple but powerful formalism for defining transition systems of various kinds, and operations on them. SOS specifications are usually presented as families of inference rules. This presentation is simple and intuitive, but a bit ad-hoc and difficult to generalize. Bialgebras and distributive laws are more abstract and more mathematical notion of well-behaved SOS specification, based on coalgebra as an abstract theory of transition systems.
I will present the basics of the bialgebraic approach to SOS, and a coalgebraic approach to modal logics that can be used to define properties of transition systems. I will then show how to combine both approaches to derive logical distributive laws, a general theory of logical compositionality on SOS-defined systems.
The course will use some basic notions of category theory: categories, functors, natural transformations, and a little bit of monads. I will introduce these notions as needed.
The plan of the course is as follows:
– Classical SOS theory: labeled transition systems, bisimulations, Hennessy-Milner logic, SOS rules, GSOS and other formats
– Basics of category theory and coalgebra
– Coalgebraic modal logic by dual adjunctions
– Distributive laws, bialgebras, abstract GSOS
– Logical distributive laws
Machine Learning Techniques and Selected Applications for Big Data
Title: Machine Learning Techniques and Selected Applications for Big Data
Lecturer: Stan Matwin (Dalhousie University, Canada)
Period: February 22, 25, 29 – March 3, 7, 10, 14, 17, 21, 24 2016
Timetable: Mon. 11:00-13:00 Thu. 14:00-16:00
Place: Department of Computer Science Sala “seminari ovest”
Stan Matwin is a Professor and Canada Research Chair in the Faculty of Computer Science at Dalhousie University, Canada, where he directs the Institute for Big Data Analytics. He is also a Professor at the Institute of Computer Science, Polish Academy of Sciences. His research interests are in text analytics, data mining, as well as in data privacy. Author and co-author of more than 250 research papers and articles, Stan is a former President of the Canadian Artificial Intelligence Society, a member of the Scientific Council of the Polish Artificial Intelligence Society, and a member of Association Francaise pour l’Intelligence Artificielle.
1. Intro (def, challenges, nosql etc.) 2h
2. Linear methods 2h
3. Bayesian Methods 3h
4. Stream Data Processing: VFDTs 2h
5. Vizualization: basics, examples 3h
6. Privacy for Big Data: data summaries (scripts, Bloom filters), ABAC approaches (Acumulo) 3h
7. Applications: Oceans 2h
8. Applications: Big Data in the Public Sector 2h
9. Data tagging challenges for Big Data: crowdsourcing, reCaptcha 1h