Bimonthly    Since 1986
ISSN 1000-9000(Print)
CN 11-2296/TP
Indexed in:
Publication Details
Edited by: Editorial Board of Journal Of Computer Science and Technology
P.O. Box 2704, Beijing 100190, P.R. China
Sponsored by: Institute of Computing Technology, CAS & China Computer Federation
Undertaken by: Institute of Computing Technology, CAS
Distributed by:
China: All Local Post Offices
Other Countries: Springer
  • Table of Content
      10 November 1998, Volume 13 Issue 6 Previous Issue    Next Issue
    For Selected: View Abstracts Toggle Thumbnails
    Playing Games and Proving Properties ofConcurrent Systems
    Colin Stirling;
    Journal of Computer Science and Technology, 1998, 13 (6): 482-. 
    Abstract   PDF(42KB) ( 1079 )   Chinese Summary
    References | Related Articles | Metrics
    Some Notes on Graph Automata, TilingSystems and Partition Logic
    Shen Enshao;
    Journal of Computer Science and Technology, 1998, 13 (6): 483-489. 
    Abstract   PDF(357KB) ( 1428 )   Chinese Summary
    Introduce heuristically the newly definitioll (W. Thomas) for graph automata - using"tiles" to simulste the extension (over dag's) of the classical notions of transition moves; proposea sufficient condition for when graph automata can be reduced to (simpler) tiling systerms, whichis a generalisation of a Thomas' result; and finally study the logic sepcification of tiling systems(paticularly, over picture languages) by (existential) monadic partition logic, instead of theususal and stronger framework (E)MSQ.
    References | Related Articles | Metrics
    Process Calculifor Describing Distributed Systems
    Matthew Hennessy;
    Journal of Computer Science and Technology, 1998, 13 (6): 490-. 
    Abstract   PDF(31KB) ( 1101 )   Chinese Summary
    References | Related Articles | Metrics
    Simply-typed Underdeterminism
    Ewen Denney;
    Journal of Computer Science and Technology, 1998, 13 (6): 491-508. 
    Abstract   PDF(841KB) ( 1542 )   Chinese Summary
    An extension of the simply-typed lambda calculus with constructs for expressing a notioncalled underdeterminism is studied. This allows us to interpret notions of stub and skeletonused in top-down program development. We axiomatise a simple notion of program refinement,and give a semantics, for which the calculus is proved sound and complete.
    References | Related Articles | Metrics
    Calculi for Concurrent Processes
    Gerard Boudol;
    Journal of Computer Science and Technology, 1998, 13 (6): 509-. 
    Abstract   PDF(48KB) ( 1143 )   Chinese Summary
    Related Articles | Metrics
    Reaction Graph
    Fu Yuxi;
    Journal of Computer Science and Technology, 1998, 13 (6): 510-530. 
    Abstract   PDF(881KB) ( 1249 )   Chinese Summary
    The paper proposes reaction graphs as graphical representations of computational objects.A reaction graph is a directed graph with all its arrows and some of its nodes labeled. Compu-tations are modeled by graph rewriting of a simple nature. The basic rewriting rules embodythe essence of both the communications among processes and cut-eliminations in proofs. Cal-culi of graphs are identified to give a formal and algebraic account of reaction graphs in thespirit of process algebra. With the help of the calcu…
    References | Related Articles | Metrics
    An invitation to Friendly Testing
    David de Frutos-Escrig; Luis Liana-Diaz; Manuel Nunez;
    Journal of Computer Science and Technology, 1998, 13 (6): 531-545. 
    Abstract   PDF(408KB) ( 1261 )   Chinese Summary
    We present a new testing semantics, called friendly testing, whose main property is thatthe induced preorder between processes fr is consistent with the conformance relation, andso we have, for instance, a b fr a fr a + b. The new theory is strongly based on De Nicola& Hennessy's work on testing. Friendly tests are defined exactly as in their work, except thatinternal actions are not allowed. However, in order to obtain the desired notion of friendlytesting this restriction is not enough and we also have to…
    References | Related Articles | Metrics
    A Crash Course in λ-Calculus
    Journal of Computer Science and Technology, 1998, 13 (6): 546-. 
    Abstract   PDF(40KB) ( 1017 )   Chinese Summary
    Related Articles | Metrics
    Anothr Definition of Order-Sorted Algebra
    He Ziqiang;
    Journal of Computer Science and Technology, 1998, 13 (6): 547-551. 
    Abstract   PDF(149KB) ( 1277 )   Chinese Summary
    In this paper the definition of order-sorted algebra is generalized by introducing transforma-tion functions between subtypes and supertypes. According to our definition, a type needn'tbe a subset of its supertype and a record model may form an order-sorted algebra. A newdefinition of equation is given. It has also been proved that equational theories and describingsingle inheritance have the initial model.
    References | Related Articles | Metrics
    An Overview of Duration Calculus
    Zhou Chaochen;
    Journal of Computer Science and Technology, 1998, 13 (6): 552-. 
    Abstract   PDF(47KB) ( 1081 )   Chinese Summary
    Related Articles | Metrics
    Formal Derivation of Graph AlgorithmicPrograms Using Partition-and-Recur
    Xue Jinyun;
    Journal of Computer Science and Technology, 1998, 13 (6): 553-561. 
    Abstract   PDF(412KB) ( 1265 )   Chinese Summary
    In this paper, we derive, by presenting some suitable notations, three typical graph aLgorithms and corresponding programs using a unified approach, partition-and-recur. We putemphasis on the derivation rather than the algorithms themselves. The main ideas and lugesnutty of these algorithms are revealed by formula deduction. Success in these examples givesus more evidence that partition-and-recur is a simple and practical approach and developingenough suitable notations is the key in designing and deriving …
    References | Related Articles | Metrics
    Explicit Substitutions: A Short Survey
    Pierre-Louts Curien;
    Journal of Computer Science and Technology, 1998, 13 (6): 562-563. 
    Abstract   PDF(91KB) ( 1338 )   Chinese Summary
    References | Related Articles | Metrics
    Dependent Type System with Subtyping (I)Type Level Transitivity Elimination
    Chen Gang;
    Journal of Computer Science and Technology, 1998, 13 (6): 564-578. 
    Abstract   PDF(675KB) ( 1305 )   Chinese Summary
    Dependent type systems are the basis of many proof development environments. In Aspinalland Compagnoni's paper, a system λP≤ is proposed as a subtyping extension of the first orderdependent type system λP (also called An). λP≤ has nice meta-theoretic properties includingsubject reduction and decidability. In this article, v,e give a reformulation of λP≤ t called λII≤.The advantages of λII< include: type level transitivity elimination property and pretypesbasedsubtyping system. These features considerably fa…
    References | Related Articles | Metrics
    Structures Definable in Polymorphism
    Fu Yuxi;
    Journal of Computer Science and Technology, 1998, 13 (6): 579-587. 
    Abstract   PDF(440KB) ( 1363 )   Chinese Summary
    Encodings in polymorphism with finite product types are considered. These encodings aregiven in terms of I-algebras. They have the property that the ground terms are precisely theclosed normal terms of the encoded types. The proof of a well-known result is transplantedto the setting and it is shown why weak recursion is admissible. The paper also shows how tocarry out the dual encodingS using the existential quantifier.
    References | Related Articles | Metrics
    Verifying Automata Specification of Distributed Probabilistic Real-Time Systems
    Luo Tiegeng; Chen Huowang; Wang Bingshan; Wang Ji; Gong Zhenghu; Qi Zhichang;
    Journal of Computer Science and Technology, 1998, 13 (6): 588-596. 
    Abstract   PDF(437KB) ( 1672 )   Chinese Summary
    In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equiv...
    References | Related Articles | Metrics
    Program Constructionby Verifying Specification
    Lin Hong; Chen Guoliang;
    Journal of Computer Science and Technology, 1998, 13 (6): 597-607. 
    Abstract   PDF(481KB) ( 1312 )   Chinese Summary
    A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used…
    References | Related Articles | Metrics
    Experimental Study on Strategy of CombiningSAT Algorithms
    Lu Weifeng; Zhang Yuping;
    Journal of Computer Science and Technology, 1998, 13 (6): 608-614. 
    Abstract   PDF(321KB) ( 1427 )   Chinese Summary
    The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems. Different kinds of SAT algorithmsall have their own hard instances respectively. Therefore, to get the better performance onall kinds of problems, SAT solver should know how to select different algorithms according tothe feature of instances. In this paper the differences of several effective SAT algorithms areanalyzed and two new parameters gb and & are proposed…
    References | Related Articles | Metrics
    ρ Graph: Rendezvous Ordering Graph forAda Concurrent Programs
    wang Zhenyu;
    Journal of Computer Science and Technology, 1998, 13 (6): 615-622. 
    Abstract   PDF(342KB) ( 1380 )   Chinese Summary
    In disciplined Ada software development and maintenance, an adequate and suitable graphical representation for concurrency is important. To describe rendezvous ordering, tasking andexecuting flow of tasks, p graph--Rendezvous Ordering Graph is presenced in this paper. pgraph is a kind of-hierarchical oriented graph with nodes representing rendezvouses and edgesshowing'ordering relations between rendezvouses as well as flow of tasks. It can be used insoftware understanding, design description and documentati…
    References | Related Articles | Metrics
  Journal Online
Just Accepted
Top Cited Papers
Top 30 Most Read
Paper Lists of Areas
Special Issues
   ScholarOne Manuscripts
   Log In

User ID:


  Forgot your password?

Enter your e-mail address to receive your account information.

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved