Voices of CANTE
Workshop on Descriptional and Computational Complexity of Formal Languages
15
Talk by José Nuno Oliveira, September 19, 14:30
11
Title: Software components as monadic, weighted Mealy machines in typed linear algebra
Speaker: José Nuno Oliveira (Universidade do Minho)
Time: September 19, 14:30
Place: S1, DCC-FCUP
Abstract:
The propagation of faults in component-based software (CBS) systems is a relevant topic in current research on software architecture and software certification. However, traditional CBS programming considers risk evaluation a posteriori, once the implemented software is subject to fault injection and other simulation techniques. In this talk we advocate that risk of failure be considered at the early stages of the design using a number of combinators which includes probabilistic choice between 'good' and 'bad' behaviour. Such combinators are implemented in Haskell on top of a probabilistic functional programming library, which makes it possible to animate and simulate faults and their propagation. Their quantitative semantics is expressed in the adjoint category of left stochastic matrices, using matrix point-free notation and calculus. This makes it possible to "internalize" the quantitative semantics of (faulty) components just by changing from the category of sets to suitable categories of matrices, while retaining the original formulae. The main difference resides in the weakness of products in the latter and absence of 'uniform copying operations', which makes one's life harder compared to the original coalgebraic component calculus - a subject of on-going research. (Joint work with L.S. Barbosa.)
José Nuno Oliveira is a professor at the Department of Informatics, School of Engineering of University of Minho in Portugal. His research interests include formal methods, algebra of programming and program calculation, and functional programming. He aims at improving scientific standards in software design through formal methods and calculational techniques. These include the application of mathematical transforms in refactoring and improving existing software theories.
Talk by Jean-Christophe Filliâtre, April 18, 11:00
09
Title: Deductive Program Verification with Why3
Speaker: Jean-Christophe Filliâtre, CNRS - Université Paris-Sud
Time: April 18, 2013, 11:00
Place: S2, DCC - FCUP
Abstract:
Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs.
Regarding the former, Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. Regarding the latter, Why3 comes with a powerful programming language featuring recursive functions, local bindings, pattern matching, exceptions, and records with possibly mutable fields. Aliasing are excluded by type checking to allow the computation of natural verification conditions through a weakest precondition calculus.
Jean-Christophe Filliâtre obtained his PhD in Computer Science in 1999 and he is a CNRS researcher at Université Paris-Sud since 2001. His research interests include theorem provers architectures, functional programming, higher-order logic, mechanical verification of imperative programs. Currently his main research activity is on deductive program verification.
Talk by José Carlos Espírito Santo, Março 22, 15:30
13
Title: CBN, CBV, and the Intuitionistic Asymmetry
Speaker: José Carlos Espírito Santo
Time: March 22, 15:30
Place: S3 - DCC - FCUP
José Carlos Espírito Santo has a PhD (2002) in Computer Science at the University of Edinburgh. He is a professor at the Department of Mathematics of the School of Sciences of University of Minho and a researcher at the group Proof Systems and Programming, within project Algebra, Logic, and Computation of Center of Mathematics of University of Minho. His research interests include structural proof theory, Curry-Howard correspondence, and lambda-calculus.
Abstract: In this talk I return to the beloved troika of computer science: call-by-name, call-by-value, and the lambda-calculus. Proof theory discovered that the boolean duality of classical logic extends to a duality between CBN and CBV. I will rather focus on the computational consequences of the intuitionistic asymmetry between hypothesis and conclusion.
Talk by Luís Miguel Pinho, February 20, 14:00
05
Title: Concurrency and parallelism in real-time embedded systems
Speaker: Luís Miguel Pinho
Time: February 20, 14:00
Place: S2 - DCC - FCUP
Luis Miguel Pinho has a MSc (1997) and a PhD (2001) in Electrical and Computer Engineering at the University of Porto. He is Coordinator Professor at the Department of Computer Engineering - School of Engineering of the Polytechnic Institute of Porto, and Vice-Director and Research Associate at the CISTER research unit, where he currently leads the real-time software research line. Miguel is/was Coordinator of CooperatES and Reflect FCT-funded Research Projects, and CISTER Coordinator of RESCUE, MethoDES and TERRA FCT projects; he was also team scientific leader in FP5 NNES project REMPLI and is team coordinator in the Artemis ENCOURAGE project.
The concurrency and predictability challenges associated with
real-time embedded systems are being exacerbated by the increasingly
dominance of multi-core and many-core platforms. These platforms allow
combining in the same system applications with a diversity of timing
requirements, and are also popularizing the ability to execute parallelized
real-time tasks.
This tendency for even larger number of processor cores is impacting the way
systems are developed, as software performance and correctness must rely on
sound techniques to design and execute concurrent software in parallel. This
talk will present some of the challenges faced when trying to make use of
this cheaply available computational power in real-time embedded systems.
Talk by Pedro Vasconcelos, November 9, 2012, 14:30
05
Title: A tour of Haskell (or: How to be lazy with class) Part II
Speaker: Pedro Vascocelos, LIACC-DCC FCUP
Time: November 16, 14:30
Place: FC029 - DCC - FCUP
Haskell is the world's leading purely-functional programming language and offers radically different approaches to writing computer programs, in particular, to ensure correctness and to exploit multi-core parallelism.
In this series of two talks I want to show how programming in Haskell can be fun and practical using some hands-on examples
The preliminary program is as follows:
Part II
* monads and side-effects
* testing with QuickCheck
* purely functional parallelism (example: a parallel K-means algorithm)
* optimization and profiling
Talk by Pedro Vasconcelos, November 2, 2012, 14:30
18
Title: A tour of Haskell (or: How to be lazy with class) Part I
Speaker: Pedro Vascocelos, LIACC-DCC FCUP
Time: November 2, 14:30
Place: CC02 - FCUP
Haskell is the world's leading purely-functional programming language and offers radically different approaches to writing computer programs, in particular, to ensure correctness and to exploit multi-core parallelism.
In this series of two talks I want to show how programming in Haskell can be fun and practical using some hands-on examples
The preliminary program is as follows:
Part I
- purity
- types
- immutable data
- higher-order functions
- programming with data transformations (example: a simple assembler/disassembler)
Talk by Janusz Brzozowski, October 8, 2012, 14:30
26
Title: Quotient Complexities of Atoms of Regular Languages
Speaker: Janusz Brzozowski (University of Waterloo, ON, Canada)
Time: October 10, 14:30
Place: M004 - FCUP
Abstract: An atom of a regular language \(L\) with \(n\) (left) quotients is a non-empty intersection of uncomplemented or complemented quotients of \(L\), where each of the \(n\) quotients appears in a term of the intersection. The quotient complexity of \(L\), which is the same as the state complexity of \(L\), is the number of quotients of \(L\). We prove that, for any language \(L\) with quotient complexity \(n\), the quotient complexity of any atom of \(L\) with \(r\) complemented quotients has an upper bound of \(2^n-1\) if \(r=0\) or \(r=n\), and \(1+\sum_{k=1}^{r} \sum_{h=k+1}^{k+n-r} C_{h}^{n} \cdot C_{k}^{h}\) otherwise, where \(C_j^i\) is the binomial coefficient. For each \(n\ge 1\), we exhibit a language whose atoms meet these bounds.
Janusz (John) Brzozowski is a Distinguished Professor Emeritus in the David R. Cheriton School of Computer Science at the University of Waterloo. He is renowned for his fundamental work on circuit theory and automata theory, and, in particular, on regular expressions and on syntactic semigroups of formal languages. He has published more than 200 papers in the areas of theory of languages and automata, asynchronous circuits, and testing. He has written two books: Digital Networks (Prentice-Hall, 1976), and Asynchronous Circuits (Springer-Verlag, 1995). His current research interests are in the theory of automata and formal languages, particularly in descriptional complexity issues for regular languages.
Talk by Janusz Brzozowski, October 3, 2012, 15:30
27
Title: Theory of Átomata
Speaker: Janusz Brzozowski (University of Waterloo, ON, Canada)
Time: October 3, 15:30
Place: FC 029 (A2), DCC-FCUP
Abstract: We show that every regular language defines a unique nondeterministic finite automaton (NFA), which we call “átomaton'', whose states are the “atoms'' of the language, that is, non-empty intersections of complemented or uncomplemented left quotients of the language. We describe methods of constructing the átomaton, and prove that it is isomorphic to the normal automaton of Sengoku, and to an automaton of Matz and Potthoff. We study “atomic'' NFA's in which the right language of every state is a union of atoms. We generalize Brzozowski's double-reversal method for minimizing a deterministic finite automaton (DFA), showing that the result of applying the subset construction to an NFA is a minimal DFA if and only if the reverse of the NFA is atomic.
Janusz (John) Brzozowski is a Distinguished Professor Emeritus in the David R. Cheriton School of Computer Science at the University of Waterloo. He is renowned for his fundamental work on circuit theory and automata theory, and, in particular, on regular expressions and on syntactic semigroups of formal languages. He has published more than 200 papers in the areas of theory of languages and automata, asynchronous circuits, and testing. He has written two books: Digital Networks (Prentice-Hall, 1976), and Asynchronous Circuits (Springer-Verlag, 1995). His current research interests are in the theory of automata and formal languages, particularly in descriptional complexity issues for regular languages.
Talk by Alexandra Silva May 11, 2012, 15:30
04
Title: Brzozowski’s algorithm (co)algebraically
Speaker: Alexandra Silva (Radboud U. Nijmegen/HASLab)
Time: May 11, 15:30
Place: S3, DCC-FCUP
Abstract: We give a new presentation of Brzozowski’s algorithm to minimize finite automata, using elementary facts from universal algebra and coalgebra, and building on earlier work by Arbib and Manes on the duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations.
Alexandra Silva was undergraduate student at Universidade do Minho. In 2011, she was awarded the IBM Scientific Prize 2010, for her Phd. thesis on Kleene Coalgebra from the U. of Nijmegen. Currently she is an assistant professor at the Institute for Computing and Information Science of the Radboud University Nijmegen.
Talk by Ana Paula Tomás, 14:00, March 16, 2012
03
Title: On the enumeration of column-convex permutominoes.
Speaker: Ana Paula Tomás (CMUP)
Time: March 16 14:00
Place: S3, DCC-FCUP
Abstract:A polyomino is an edge-connected set of unit squares on a regular square lattice. It is row-convex (column-convex) if all its rows (columns) are connected sets, and convex if it is both row-convex and column-convex. The enumeration problem for general polyominoes is still open, although
positive results were achieved for special classes of polyominoes, which satisfy convexity or directness conditions. A permutomino of size $r+1$ is a simply-connected polyomino such that its boundary is an orthogonal polygon with $r$ reflex vertices with exactly one edge in each line of the \((r+1)(r+1)\) minimal bounding box that contains it (a.k.a., a grid orthogonal polygon with \(2r+4\) vertices). A closed formula for the number of convex permutominoes of size \(r+1\) is known, but not for the column-convex permutominoes (Beaton et al., FPSAC 2011).
In this talk, I will present a recursive method for the direct enumeration of permutominoes by size, and its specialization for the column-convex permutominoes, from whichwe can deduce a simple recurrence relation for the number of column-convex permutominoes of a given size.
Talk by Ana Loureiro 14:30. April 20, 2012
04
Title: Integral composite powers of differential operators associated to certain polynomial sequences.
Speaker: Ana Loureiro (CMUP)
Time: April 20 14:30
Place: S3, DCC-FCUP
Abstract: Polynomial sequences generated by integral powers of first and second order differential operators with polynomial coefficients will be the issue. More precisely, the focus will lie on their connection with well known orthogonal polynomial sequences along with their foremost structural properties. We will start by analysing the cases in which the aforementioned differential operator is of first order, bringing into analysis polynomial sequences associated to the classical linear functionals of Hermite, Laguerre, Bessel and Jacobi. Afterwards, the discussion will proceed towards the analysis of polynomial sequences generated by second order differential operators, which brings up the open problem of characterizing orthogonal polynomial sequences with respect to certain positive definite linear functionals. The Kontorovich-Lebedev transform and the central factorials will be an asset to attain our goals.
Beneath the results is the algebraic theory of orthogonal polynomials, not disregarding the contribution of some combinatorial analysis essentially centered around generalizations and extensions of the Stirling numbers.
Talk by Pedro Silva, 14:30, January 23, 2012
07
Title: Wreath product decompositions: an apology
Speaker: Pedro Silva (CMUP)
Time: January 23 14:30
Place: DCC-FCUP
Abstract: The wreath product stormed into automata theory in the sixties through the classical Krohn-Rhodes decomposition theory, which changed the perspective of the whole theory of rational languages and initiated a new era of deep connections with algebra, particularly semigroup theory. This misterious operator has a very simple and natural
formulation in terms of actions on trees, and it is only natural that it keeps appearing involved in various subjects relevant to theoretical computer science. Such examples include:
(1) Krohn-Rhodes type decomposition theorems for infinite semigroups.
(2) The exotic world of the fractal-like automata groups.
(3) The bimachine approach to Turing machine computation.
Talk by Jorge Sousa Pinto, November 30, 2011, 17:00
14
Title: Verification Conditions for Single-assignment Programs
Speaker: Jorge Sousa Pinto (Departamento de Informática da Universidade do Minho)
Time: November 30 16:00
Place: S3, DCC-FCUP
Abstract: A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this paper we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas.
Talk by Ivone Amorim, October 26, 2011, 17:00
15
Title: Sobre a invertibilidade de Autómatos Finitos Lineares
Speaker: Ivone Amorim
Time: October 26 17:00
Place: S3, DCC-FCUP
ResumoA criptografia de chave pública baseada em autómatos finitos assenta em resultados que caracterizam alguns tipos de autómatos invertíveis,
assim como em técnicas para construir um autómato invertível e, simultaneamente, um seu inverso. Torna-se, portanto, fundamental ter uma boa caracterização destes autómatos.
Esta apresentação centra-se no problema da invertibilidade dos autómatos lineares. Começaremos por definir os conceitos básicos, apresentando-se de seguida alguns resultados de Renji Tao. Por fim, será apresentada uma nova condição para verificar se um autómato linear com memória é fracamente invertível com atraso \(\tau\). Esta condição usa a forma normal de Smith de uma matriz polinomial, o que é um bom indicador das suas potencialidades para fins criptográficos. A partir da demonstração deste resultado obtém-se ainda um novo método para construir um inverso com atraso \(\tau\) de um autómato finito linear invertível.
Ivone Amorim é aluna do Programa Doutoral em Ciência de Computadores
Talk by André Pedro, July 4 2011, 14:30
23
Title: Aprendizagem de processos semi-Markovianos generalizados: dos sistemas de eventos discretos estocásticos aos testes e à verificação
Speaker: André Pedro
Time: July 4 14:30
Place: S2, DCC-FCUP
Resumo Sistemas estocásticos de eventos discretos (SDES) são uma importante subclasse de sistemas (à luz da teoria dos sistemas). Estes têm sido usados, em particular na indústria, para analisar e modelar uma grande variedade de sistemas reais, como por exemplo sistemas de produção, sistemas computacionais, sistemas de tráfego e sistemas híbridos. Este trabalho mostra como aprender e usar os processos semi-Markovianos generalizados (GSMP) como processo de modelação de SDES na ausência da definição destes últimos. Sendo os GSMP uma classe de processos que contém os processos estocásticos que não contenham variáveis latentes, introduziremos a noção de aprendizagem de SDES e demonstraremos a correcção do processo de aprendizagem e as suas implicações para a convergência do método. Apresentamos a seguir exemplos práticos do uso desta metodologia. Em particular, mostramos como utilizar os GSMP aprendidos como oráculos de teste num contexto de validação ou como modelos num cenário de model checking probabilístico.
André Pedro é aluno do Mestrado em Engenharia Informática da Universidade do Minho
Talk by Emanuele Rodaro, June 15 2011, 14:30
01
Title: Finitely generated synchronizing automata
Speaker: Emanuele Rodaro, Centro de Matemática da Universidade do Porto
Time: June 15 , 14h30,
Place: S2, DCC-FCUP
Abstract:
A deterministic finite-state automaton A on the alphabet \(\Sigma\) is said to be synchronizing if there is a synchronizing word, i.e. a word that takes all the states of the automaton A to a particular one. We consider the class of synchronizing automata whose language of synchronizing words is finitely generated as a two-sided ideal in \(\Sigma^\star\) and we call such automata finitely generated. We show that for such class of automata, Cerny conjecture holds with a linear upper bound. Whereas testing if a given DFA is synchronizing is a polynomial time task, we show that recognizing finitely generated automata is a PSPACE-complete problem.
Emanuele Rodaro has a Phd degree in Mathematics at “Università degli Studi di Milano”, 2006. Since then he has been a postdoctoral researcher in several european research centers. His research area is located at the border between algebra, combinatorics and theoretical computer science. His main interest concerns the theory of semigroups and its role in the theory of automata and formal languages.
Talk by Vladimir Komendantsky, May 4, 2011 14:30
27
Title: Computational specification in a finite domain: A case study with regular expressions.
Speaker: Vladimir Komendantsky, School of Computer Science, St. Andrews Univ.
Time: 14h30m, 4/05/2011
Room: S2, DCC - FCUP
Abstract:
I work to provide a toolbox for provably-correct computations in a proof assistant for problems such as "What is a function, if there are any, coercing a regular expression E to a regular expression F?" If proof assistants are concerned, one usually understands the term "program specification" as a problem of constructing a function that computes an object and, at the same time, provides a proof that this object satisfies a certain property. This kind of dependent pair is known under the name of "sigma-type". It is a bit too general for complex studies involving layers of nested structures. We have to practice another, more effective approach in cases when some parts of the domain of discourse are known to be finite (like a finite alphabet of a language). Then, for example, we can effectively convert between a potentially infinite language denoted by a regular expression and a finite matrix of partial derivatives of this regular expression. This method reduces profoundly the complexity of proofs.
Vladimir Komendantsky has a Phd degree from the Russian Academy of Sciences in 2003. Since then he was a postdoctoral researcher in several european research centers. His main research interests are interactive theorem provers based on dependent type theories; logic and functional programming; and formal program specification. He is currently a researcher in the project "SImPL: Specification and Implementation of Pattern Languages", School of Computer Sciencce, St Andrews University
Talk by Cezar Campeanu
11
Title: New Directions in Cover Automata Theory
SPEAKER:
Cezar Câmpeanu, Dept. of Computer Science and Information Technology
University of Prince Edward Island, Canada
TIME and LOCAL: 11/02/2011, 14h30m DCC-FCUP, S02
Abstract:
Cover automata and similarity relations have been studied for more than 10 years.
Even though the feeling that such an object may be useful and could be constructed was in some way present in papers from the 60's, the first rigorous formal definition, as well as a clear minimization algorithm, was presented at WIA98 for the very first time.
In this talk we introduce the concept of cover languages, cover automata and similarity relations, along with a summary of the most important results. It is emphasized the difficulty of obtaining existing results and the challenges for getting new ones. A list of open problems and suggestions of solving them is, as well, included.
Slides of the Talk
Descriptive Complexity and Computational Complexity
21
Armando Campos e Matos will give a talk, on June 23, 14:30, at room 3 of DCC.
Title: Descriptive Complexity and Computational Complexity
Summary:
We present a summary of well known results on the relationship between Descriptive Complexity and Computational Complexity. A short survey of Finite Model Theory is also included.