Research group VERIF
Last update 15 December, 2009
We are a small part of the division Embedded Systems of the
Center of Applied Cybernetics (CAK)
http://c-a-k.cz/
(which is a research center supported by the Czech Ministry
of Education, project 1M0567, planned for years 2005 - 2009)
Short description:
The group consists of three people in Dept of Computer Science, FEI VSB-TU Ostrava,
who work in the research area which can be classified as verification
of systems.
The main current interest focuses on algorithms deciding bisimilarity
on various classes of processes, and related questions.
Current members:
Activities (in CAK, and related to CAK, since 2005)
2005
-
Main CAK-publications
-
Jancar P., Sawa Z.:
On distributed bisimilarity over Basic Parallel Processes;
in (Pre)proc. of the 4th Intern. Workshop
on Automated Verification of Infinite-State Systems - AVIS'05
(affiliated with ETAPS'05), Edinburgh, GB, April 2005
\\
Revised version submitted in August 2005 to the respective
ENTCS-volume (devoted to AVIS 2005)
-
Mark Schaefer, Walter Vogler, Petr Jancar:
Determinate STG Decomposition of Marked Graphs.
In Proc:
Applications and Theory of Petri Nets 2005
26th International Conference, ICATPN 2005, Miami, FL, June 20-25, 2005,
Series: Lecture Notes in Computer Science, Vol. 3536
Ciardo, Gianfranco; Darondeau, Philippe (Eds.)
Springer Verlag 2005,
p. 365 - 384 ISBN: 3-540-26301-2
-
Jancar P., Kot M., Sawa Z.:
Notes on Complexity of Bisimilarity between BPA and BPP;
accepted talk on EXPRESS'05
(12th International Workshop on
Expressiveness in Concurrency),
27 August, 2005 San Francisco, USA
(affiliated with CONCUR 2005)
-
Sawa Z., Jancar P.:
Behavioural Equivalences on Finite-State Systems are PTIME-hard;
Computing and Informatics (CaI),
Vol. 24, No. 5, 2005, pp. 513 - 528,
(ISSN 1335-9150)
-
Talks by PJ, ZS, MK at
Embedded systems colloquium 2005 ,
Prague, 26 Oct 2005
-
Further (CAK-related) publications:
-
Jancar, P.: Verification of computer systems (theoretical aspects)
(in Czech); an invited talk at STTI 2005, Prague, May 2005
-
Sawa, Z.: Hardness of equivalence testing at
finite state systems (in Czech); in Proc. STTI 2005, Prague, May 2005, 42-43
-
Sawa, Z.: Complexity and Decidability of Some Equivalence-Checking Problems.
PhD thesis, defended at FEI, Techn. Univ. Ostrava, May 2005
-
Sawa, Z., Kot, M.: Bisimulation equivalence of a BPP and a finite-state
system can be decided in polynomial time. In Electronic Notes in
Theoretical Computer Science, 2005, vol. 138, No. 3, p. 49-60
-
Jancar P.:
Some techniques and results in deciding bisimilarity;
invited talk at the Verification seminar, ULB Brussels, Belgium,
December 16, 2005
-
Kot, M.: Regularity of BPP is PSPACE-complete. In Proceedings of the
3th annual workshop WOFEX 2005. Ed. Václav Sná¹el,
Technical University of Ostrava, 2005, p. 393-398
(ISBN 80-248-0866-8)
-
Membership (P. Jancar) in and reviewing work (PJ, ZS, MK) for
Program Committees of:
- FoSSaCS'05 8th
International Conference on Foundations of Software Science and
Computation Structures
- ATPN'05
26th International Conference On Application and Theory
of Petri Nets and Other Models of Concurrency
- Infinity'05
7th International Workshop on Verification of Infinite-State Systems
2006
-
Main CAK-publications
-
Jancar P., Srba J.: Undecidability Results for Bisimilarity
on Prefix Rewrite Systems; in Aceto, L., Ingolfsdottir, A. (Eds.)
Foundations of Software Science and Computation Structures,
9th International Conference, FOSSACS 2006.
Vienna, Austria, March 2006, Proceedings.
Lecture Notes in Computer Science. Volume 3921, Springer 2006,
pp. 277--291
-
Esparza J., Jancar P., Miller A.:
On the Complexity of Consistency and Complete State Coding
for Signal Transition Graphs;
in Proceedings of the 6th International Conference on Application
of Concurrency to System Design (ACSD 2006). Turku, Finland, June
2006, IEEE Computer Society 2006, pp. 47--56
-
Sawa Z., Jancar P.:
History Preserving Bisimilarity on Basic Parallel Processes;
in Proceedings of TAAPSD'06, Kiev, Ukraine, December 5-8, 2006
-
Kot M.: Complexity of some Bisimilarity Problems between BPP and BPA or Finite-State System.
In Proceedings of MOVEP 2006, Bordeaux:LaBRI, University of Bordeaux-1 , 2006, p. 318-323
-
Further (CAK-related) publications:
-
Jancar, P.: Verification of computer systems (some theoretical aspects);
an invited talk at ECI'06 (Sept. 20.-22., 2006, Kosice-Herlany,
Slovakia)
-
Membership (P. Jancar) in and reviewing work (PJ, ZS, MK) for
Program Committees of:
- ATPN'06
27th International Conference On Application and Theory
of Petri Nets and Other Models of Concurrency
- MoVeP'06
MOdelling and VErifying parallel Processes
- ICTAC'06
3rd International Colloquium On Theoretical Aspects
of Computing
- MEMICS'06
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
2007
-
Publications
-
Jancar P., Sawa Z.: A Note on Emptiness for Alternating Finite
Automata with a One-Letter Alphabet;
Information Processing Letters 104: 164-167.
Elsevier 2007,
ISSN 0020-0190 (Impact Factor~0.532)
-
Esparza J., Jancar P., Miller A.: On the Complexity of Consistency and
Complete State Coding for Signal Transition Graphs;
to appear in the journal Fundamenta Informaticae , IOS Press,
(final version accepted in May 2007),
ISSN 0169-2968, (Impact Factor~0.586), appeared in Vol. 86, Number 3,
2008, pp. 227-253
-
Jancar P.: Bouziane's transformation of the Petri net
reachability problem and incorrectness of the related algorithm;
to appear in the journal Information and Computation
(Elsevier, Academic Press), (final version accepted in July 2007),
ISSN 0890-5401, (Impact Factor~1.107),
appeared in Vol. 206 (2008), pp. 1259-1263
-
Jancar P., Mraz F., Platek M., Vogel J.:
Monotonicity of restarting automata;
to appear in Journal of Automata, Languages and Combinatorics
(Univ. Magdeburg, Germany), (final version accepted in May 2007)
ISSN 1430-189X,
appeared (in 2008) in Vol. 12, Number 3, 2007, pp. 355 - 371
- Kot M.: Notes on Modeling of Real-Time Database System
V4DB in Verification Tool Uppaal.
In Proc. Memics 2007 (Oct 26-28 2007, Znojmo, CZ),
MU and TU Brno, p. 82-89, ISBN 978-80-7355-077-6
-
Talks by PJ and ZS at
Embedded systems colloquium 2007 ,
Prague, 1 Feb 2007
-
Membership (P. Jancar) in and reviewing work (PJ, ZS, MK) for
Program Committees of:
- ACSD'07
7th International Conference on
Application of Concurrency to System Design
- MEMICS'07
3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
2008
-
Publications
- (During 2008 appeared the papers [EJM], [Jan], [JMPV]
reported above in 2007.)
-
Jancar P., Srba J.: Undecidability of bisimilarity
by Defender's forcing; Journal of the ACM , Vol. 55,
Issue 1, Article No. 5, Feb 2008, 26 p., ACM (New York, USA),
ISSN:0004-5411
-
Petr Jancar, Martin Kot, Zdenek Sawa:
Normed BPA vs. Normed BPP Revisited;
in Franck van Breugel, Marsha Chechik (Eds.)
CONCUR 2008 - Concurrency Theory, 19th International Conference,
Toronto, Canada, August 19-22, 2008. Proceedings.
Lecture Notes in Computer Science 5201, Springer 2008,
pp. 434-446 (best paper award)
-
Jancar, P.: Selected Ideas Used for Decidability and
Undecidability of Bisimilarity. In Proc. Developments in
Language Theory, 12th International Conference, DLT 2008. Ed.
Ito, Masami; Toyama, Masafumi (Eds.) , Berlin:Springer-Verlag,
2008, vol. 5257, Lecture Notes in Computer Science, pp. 56-71,
ISSN: 0302-9743, ISBN: 978-3-540-85779-2 (invited talk)
-
Sawa Z., Jancar P.: Hardness of equivalence checking
for composed finite-state systems; to appear in the journal
Acta Informatica (accepted in Sep 2008)
appeared in vol. 46 (2009), No. 3, 169-191
[ http://dx.doi.org/10.1007/s00236-008-0088-x ]
-
Kot, M.: Modeling Real-Time Database Concurrency Control Protocol Two-Phase-Locking in Uppaal. Ed. M. Ganzha, M. Paprzycki, T. Pe³ech-Pilichowski, Los Alamitos, CA:IEEE Computer Society Press, 2008, p. 673-678, Polskie Towarzystwo Informatyczne, ISBN 978-83-60810-14-9, ISSN 1896-7094
-
Membership (P. Jancar) in and reviewing work (PJ, ZS, MK) for
Program Committees of:
- FoSSaCS'08 11th
International Conference on Foundations of Software Science and
Computation Structures
- ACSD'08
8th International Conference on
Application of Concurrency to System Design
- MoVeP'08
MOdelling and VErifying parallel Processes
- MEMICS'08
4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
2009
-
Publications
- (During 2009 appeared the paper [SawaJancar]reported above in 2008.)
-
Froeschle S., Jancar P., Lasota S., Sawa Z.:
Noninterleaving bisimulation equivalences on basic parallel
processes; in journal Information and Computation
Volume 208, Issue 1, January 2010, Pages 42-62
[http://dx.doi.org/10.1016/j.ic.2009.06.001 ]
-
Kot, M.: Modeling selected real-time database concurrency control protocols in Uppaal.
In: journal Innovations in Systems and Software Engineering ,
vol. 5 (2009), No. 2, p. 129-138
[http://dx.doi.org/10.1007/s11334-009-0086-3
]
-
Membership (P. Jancar) in and reviewing work (PJ, ZS, MK) for
Program Committees of:
-
ACSD'09
9th International Conference on
Application of Concurrency to System Design
- MEMICS'09
5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
2010
-
In preparation:
-
Jancar P., Kot M., Sawa Z.:
Normed processes (submitted to a journal)
-
Jancar P., Kot M., Sawa Z.:
Bisimilarity on Basic Parallel Processes;
(in preparation for journal submission)
-
Kot M.: Modelling real-time databases .... (continuation)
-
(Dufourd C.), Finkel A., Jancar P., Schnoebelen Ph.:
Complexity of some basic problems for Petri nets with special
arcs (in preparation for journal submission)
-
Membership (P. Jancar) in and reviewing work (PJ, ZS, MK) for
Program Committees of:
- Concur'10
21st International Conference on Concurrency Theory
- ACSD'10
10th International Conference on
Application of Concurrency to System Design
- MoVeP'10
MOdelling and VErifying parallel Processes