AVISPA Seminar

Check the forthcoming talks or the log of past talks.

Past Talks

Learning During Search
Speaker: Alejandro Arbeláez Slides
Autonomous Search is a new emerging area in Constraint Programming, motivated by the demonstrated importance of the application of Machine Learning techniques to the Algorithm Selection Problem, and with potential applications ranging from planning and configuring to scheduling. This area aims at developing automatic tools to improve the performance of search algorithms to solve combinatorial problems, e.g., selecting the best parameter settings for a constraint solver to solve a particular problem instance. In this talk, we study three different points of view to automatically solve combinatorial problems; in particular Constraint Satisfaction, Constraint Optimization, and SAT problems.
Date, Time and Place: (Tuesday) November 1, 2011, 2pm. Room Teleaula 2 del edificio 317, Universidad del Valle.

Prototipo para minimización de costo en cadenas de suministro
Speaker: María Andrea Cruz Blandón Slides
Se presentarán los objetivos y fases que se han planteado para el desarrollo de la práctica investigativa, que pretende entre sus objetivos mostrar de manera web dos aplicaciones desarrolladas por estudiantes del grupo AVISPA. Entre las aplicaciones seleccionadas se encuentra el trabajo de grado de Jairo Maldonado.

Por lo anterior se introducirá al problema de las cadenas de suministro, que consiste, en las etapas que se deben de llevar a cabo para satisfacer la demanda de los clientes, preocupándose por entregar los productos en tiempos óptimos, a precios razonables, y minimizando los costos. Se presentará entonces el modelo planteado usando restricciones para dar solución a este problema.
Date, Time and Place: (Tuesday) October 4, 2011, 2pm. Room Teleaula 2 del edificio 317, Universidad del Valle.

Job Shop Scheduling & Citas terapéuticas
Speaker: Holmes Giovanny Salazar y Harvin Jessid Rengifo Slides
Job Shop Scheduling
El problema de Job Shop Scheduling consiste en plani car un conjunto de trabajos sobre un conjunto de recursos o máquinas físicas. Cada trabajo debe ser procesado una vez en todas las máquinas. Además cada trabajo consta de una cadena de tareas, donde cada tarea tiene un tiempo de procesamiento determinado.

Citas terapéuticas
En un modelo de adjudicación de citas de una clínica de rehabilitación o terapéutica, se asignan a los pacientes varias sesiones o citas en un intervalo de tiempo de nido para que los mismos sean tratados por uno o varios profesionales. Actualmente la Clínica de Rehabilitación del Valle cuenta con un sistema de asignación de citas que no se ajusta a este modelo.
Date, Time and Place: (Tuesday) September 20, 2011, 2pm. Room Teleaula 2 del edificio 317, Universidad del Valle.

Una Aproximación a las Estructuras de Eventos
Speaker: Jose Nicolas Morales
Estructuras de eventos es un formalismo de programación concurrente, el cual representa un proceso como un conjunto de ocurrencias de eventos, una de las características mas importantes es que permite representar como los eventos dependen causalmente uno de otros (true-concurrency) e identificar los puntos de la computación en los cuales se toman las decisiones (Branching-time). La importancia de este modelo radica en su posibilidad de representar comportamientos y definir equivalencias en los dominios de scott, en esta presentación se intentara reflejar exactamente eso, como sus autores en un principio encuentra la necesidad de traducir planteamientos de las redes de petri utilizando un modelo básico el cual permita migrar un esquema concurrente a teoría de dominios, esto servirá como base para el entendimiento de otras traducciones de modelos concurrentes como CCS y CSP.
Date, Time and Place: (Monday) TBC, 2008, 11am. Room TBA, Javeriana.

Spatial Logics for Concurrent Calculi
Speaker: John Alexander Vargas
The spatial logics are formalisms that can express properties of freshness, secrecy, structure and behavior of concurrent systems. With the purpose of using these logics as underlying system of the CCP calculus, I have revised the state of the art of these logics, studying their use in Mobile ambients calculus and some concurrent calculus; In this talk, I will present this study.

Specification and Verification of Concurrent Systems
Speaker: Julian E. Gutierrez
In this talk we will try to give a general idea of what Specification and Verification of Concurrent Systems mean in the context of Process Calculi. To do so, we will present a basic modelling language of concurrent systems and a modal logic for specifying some of their properties. In order to give a more comprehensive view of the study of concurrent systems, other Algebras and Logics for Processes will be also mentioned. In particular, we shall use Games both to verify behavioural equivalences such as bisimilarity and to do Model Checking. As the talk aims at motivating (potential) Avispa members to do research in this area of Theoretical Computer Science, little knowledge in Concurrency Theory is assumed, so as to make it adequate, and hopefully interesting, to students and/or researchers with different kinds of interests and background.

Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus
Speaker: Jesus A. Aranda slides (video: http://cic.puj.edu.co/~ggutierrez/seminar-01-02-2008.zip)
In [PSVV06] the authors studied the expressiveness of persistence in the asynchronous π-calculus (Aπ) wrt weak barbed congruence. The study is incomplete because it ignores the issue of divergence. We present an expressive- ness study of persistence in the asynchronous π-calculus wrt De Nicola and Hen- nessy’s testing scenario which is sensitive to divergence. Following [PSVV06], we consider Aπ and three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIAπ), the persistent-output calculus (POAπ) and persistent calculus (PAπ). In [PSVV06] the authors showed encod- ings from Aπ into the semi-persistent calculi (i.e., POAπ and PIAπ) correct wrt weak barbed congruence. We prove that, under some general conditions, there cannot be an encoding from Aπ into a (semi)-persistent calculus preserving the testing semantics. Bibliography [PSVV06] C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59-68, 2006.

Towards a Constraint-Based Framework for the Analysis of Probabilistic Reactive Systems
Speaker: Jorge A. Perez
Behavior in many systems usually combines several non-trivial phe- nomena (e.g., time, non-determinism) and depends on partial and/or unknown information. Often, partial information can be represented as constraints, and some form of probabilistic behavior is appropriate to describe uncertainty. In this work we set the grounds of a framework for modeling and verifying systems involving constraints, probabilities and time. pntcc, a timed process calculus with probabilistic choice, is proposed as description language. A probabilis- tic temporal logic provides verification capabilities over system specifications. The notion of observable behavior of a process what an environment can per- ceive from its execution is shown to provide a unified basis for reasoning about systems in both operational and logical terms. We illustrate our approach by modeling and verifying a biological system.

A Process Calculus for Universal Concurrent Constraint Programming: Semantics, Logic and Application
Speaker: Carlos A. Olarte
We introduce the Universal Timed Concurrent Constraint Program- ming (utcc) process calculus; a generalisation of Timed Concurrent Constraint Programming. The utcc calculus allows for the specification of mobile be- haviours in the sense of Milner’s pi-calculus: Generation and communication of private links. We first endow utcc with an operational semantics and then with a symbolic semantics to deal with problematic operational aspects involving infinitely many substitutions and divergent internal computations. The novelty of the symbolic semantics is to use temporal constraints to represent finitely infinitely-many substitutions. We also show that utcc has a strong connection with Pnueli’s Temporal Logic. This connection can be used to prove reachability properties of utcc processes. As a compelling example, we use utcc to exhibit the secrecy flaw of the Needham-Schroeder security protocol.

Probabilistic Extension to the Concurrent Constraints Factor Oracle Model for Music Improvisation
Speaker: Mauricio Toro (Download Slides)
Multimedia Semantic Interaction studies systems acting together with the user, to learn and update constantly, a model of the user’s behavior. For example, the machine music improvisation, where the system, simultaneously learns from the user, produces and interpretates, in real time, music sequences according to the music style the user has. The “Concurrent Constraints Factor Oracle model for Music Improvisation” uses the NTCC calculus for the concurrency control, making very easy the synchronization of the different agents by the use of constraints, but the sequences are chosen in a non-deterministic way, making impossible to predict results about the musical sequences chosen and it does not make variations to the information captured. This model is an exten- sion, allowing probabilistic choice of musical sequences and sequence variation, using the SNTCC calculus and a probabilistic extension to the Factor Oracle Algorithm to work as a probabilistic automata. In addition, we also describe the implementation of our model in a NTCC interpreter written in Commmon Lisp using GECODE that is capable of real time performance.

Keywords Factor oracle, concurrent constraints process calculus, Constraint Programming, machine learning, machine improvisation, GECODE, NTCC, SNTCC, probabilistic automata.

Orion: Software to assign time slots and resources to the courses in a University
Speaker: Ivan J. Romero
Orion is a software to assign time slots and resources to the sections courses in a University. This provide a web interface to enter the problem information in a natural way and a engine build in c++ to find the problem solution. The engine uses meta-heuristics algorithms.

ccp and event structures: towards a true concurrence semantics of stochastic, real-time ccp
Speaker: Camilo Rueda (Download Slides)
ccp calculi has provided a powerful modeling strategy for many systems. As these systems gain in complexity, compositionality and granularity begin to interfere. In systems of some complexity, atomicity of basic actions could not realistically be considered to persist in processes they compose. In the 90’s Saraswat proposed a true concurrent version of ccp and gave its semantics using trace operators. In project REACT we are considering a different strategy, namely using event structures. In this talk we discuss Saraswat’s true concurrent ccp and introduce the event structures model with its temporal extension. Then Pratt’s ”couples” representation of event structures is used to propose possible ways of giving semantics to basic ccp constructs.

grupos/avispa/seminar.txt · Última modificación: 2020/05/12 09:39 por jearias
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki